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

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