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 : β) (_ : b ∈ Encodable.decode₂ β i), f b = ⨆ (b : β), f b

theorem Encodable.iUnion_decode₂ {α : Type u_1} {β : Type u_2} [Encodable β] (f : β → Set α) : ⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.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 : β) (_ : b ∈ Encodable.decode₂ β n), f b)

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