Mathlib.Logic.Encodable.Lattice

Module docstring

{"# Lattice operations on encodable types

Lemmas about lattice and set operations on encodable types

Implementation Notes

This is a separate file, to avoid unnecessary imports in basic files.

Previously some of these results were in the MeasureTheory folder. "}

Encodable.iSup_decode₂ theorem

[CompleteLattice α] (f : β → α) : ⨆ (i : ℕ) (b ∈ decode₂ β i), f b = (⨆ b, f b)

Full source

theorem iSup_decode₂ [CompleteLattice α] (f : β → α) :
    ⨆ (i : ℕ) (b ∈ decode₂ β i), f b = (⨆ b, f b) := by
  rw [iSup_comm]
  simp only [mem_decode₂, iSup_iSup_eq_right]

Supremum over Encodable Type via Decoding

Informal description

Let $\alpha$ be a complete lattice and $\beta$ be an encodable type. For any function $f : \beta \to \alpha$, the supremum over all natural numbers $i$ and elements $b$ in the decoding of $i$ to $\beta$ of $f(b)$ is equal to the supremum of $f$ over all elements of $\beta$. That is, \[ \bigsqcup_{i \in \mathbb{N}} \bigsqcup_{b \in \text{decode}_\beta(i)} f(b) = \bigsqcup_{b \in \beta} f(b). \]

Encodable.iUnion_decode₂ theorem

(f : β → Set α) : ⋃ (i : ℕ) (b ∈ decode₂ β i), f b = ⋃ b, f b

Full source

theorem iUnion_decode₂ (f : β → Set α) : ⋃ (i : ℕ) (b ∈ decode₂ β i), f b = ⋃ b, f b :=
  iSup_decode₂ f

Union over Encodable Type via Decoding

Informal description

Let $\beta$ be an encodable type and $f : \beta \to \mathcal{P}(\alpha)$ be a function from $\beta$ to subsets of $\alpha$. Then the union over all natural numbers $i$ and elements $b$ in the decoding of $i$ to $\beta$ of $f(b)$ is equal to the union of $f(b)$ over all elements $b$ of $\beta$. That is, \[ \bigcup_{i \in \mathbb{N}} \bigcup_{b \in \text{decode}_\beta(i)} f(b) = \bigcup_{b \in \beta} f(b). \]

Encodable.iUnion_decode₂_cases theorem

{f : β → Set α} {C : Set α → Prop} (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} : C (⋃ b ∈ decode₂ β n, f b)

Full source

@[elab_as_elim]
theorem iUnion_decode₂_cases {f : β → Set α} {C : Set α → Prop} (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} :
    C (⋃ b ∈ decode₂ β n, f b) :=
  match decode₂ β n with
  | none => by
    simp only [Option.mem_def, iUnion_of_empty, iUnion_empty, reduceCtorEq]
    apply H0
  | some b => by
    convert H1 b
    simp [Set.ext_iff]

Predicate Preservation under Encoded Union Construction

Informal description

Let $β$ be an encodable type, $f : β → \mathcal{P}(α)$ a function from $β$ to sets of $α$, and $C : \mathcal{P}(α) → \text{Prop}$ a predicate on sets. If $C$ holds for the empty set and for $f(b)$ for every $b ∈ β$, then for any natural number $n$, $C$ holds for the union of $f(b)$ over all $b$ in the $n$-th decoding of $β$.

Encodable.iUnion_decode₂_disjoint_on theorem

{f : β → Set α} (hd : Pairwise (Disjoint on f)) : Pairwise (Disjoint on fun i => ⋃ b ∈ decode₂ β i, f b)

Full source

theorem iUnion_decode₂_disjoint_on {f : β → Set α} (hd : Pairwise (DisjointDisjoint on f)) :
    Pairwise (DisjointDisjoint on fun i => ⋃ b ∈ decode₂ β i, f b) := by
  rintro i j ij
  refine disjoint_left.mpr fun x => ?_
  suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]
  rintro a rfl ha b rfl hb
  exact (hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩

Pairwise Disjoint Union Preservation under Decoding for Encodable Types

Informal description

Let $β$ be an encodable type and $f : β → \text{Set } α$ be a function such that the images $f(b)$ are pairwise disjoint for all $b ∈ β$. Then for any natural number $i$, the union $\bigcup_{b ∈ \text{decode}_2 β i} f(b)$ is also pairwise disjoint when indexed by $i$.