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.iSup_decode₂ {α : Type u_1} {β : Type u_2} [Encodable β] [CompleteLattice α] (f : β → α) : ⨆ (i : ℕ), ⨆ b ∈ decode₂ β i, f b = ⨆ (b : β), f b

theorem Encodable.iUnion_decode₂ {α : Type u_1} {β : Type u_2} [Encodable β] (f : β → Set α) : ⋃ (i : ℕ), ⋃ b ∈ decode₂ β i, f b = ⋃ (b : β), f b

theorem Encodable.iUnion_decode₂_cases {α : Type u_1} {β : Type u_2} [Encodable β] {f : β → Set α} {C : Set α → Prop} (H0 : C ∅) (H1 : ∀ (b : β), C (f b)) {n : ℕ} : C (⋃ b ∈ decode₂ β n, f b)

theorem Encodable.iUnion_decode₂_disjoint_on {α : Type u_1} {β : Type u_2} [Encodable β] {f : β → Set α} (hd : Pairwise (Function.onFun Disjoint f)) : Pairwise (Function.onFun Disjoint fun (i : ℕ) => ⋃ b ∈ decode₂ β i, f b)