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.
theorem
Encodable.supᵢ_decode₂
{α : Type u_1}
{β : Type u_2}
[inst : Encodable β]
[inst : CompleteLattice α]
(f : β → α)
:
(⨆ i, ⨆ b, ⨆ h, f b) = ⨆ b, f b
theorem
Encodable.unionᵢ_decode₂
{α : Type u_1}
{β : Type u_2}
[inst : Encodable β]
(f : β → Set α)
:
(Set.unionᵢ fun i => Set.unionᵢ fun b => Set.unionᵢ fun h => f b) = Set.unionᵢ fun b => f b
theorem
Encodable.unionᵢ_decode₂_cases
{α : Type u_1}
{β : Type u_2}
[inst : Encodable β]
{f : β → Set α}
{C : Set α → Prop}
(H0 : C ∅)
(H1 : (b : β) → C (f b))
{n : ℕ}
:
C (Set.unionᵢ fun b => Set.unionᵢ fun h => f b)
theorem
Encodable.unionᵢ_decode₂_disjoint_on
{α : Type u_1}
{β : Type u_2}
[inst : Encodable β]
{f : β → Set α}
(hd : Pairwise (Disjoint on f))
:
Pairwise (Disjoint on fun i => Set.unionᵢ fun b => Set.unionᵢ fun h => f b)