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 measure_theory folder.
theorem
encodable.supr_decode2
{α : Type u_1}
{β : Type u_2}
[encodable β]
[complete_lattice α]
(f : β → α) :
(⨆ (i : ℕ) (b : β) (H : b ∈ encodable.decode2 β i), f b) = ⨆ (b : β), f b
theorem
encodable.Union_decode2
{α : Type u_1}
{β : Type u_2}
[encodable β]
(f : β → set α) :
(⋃ (i : ℕ) (b : β) (H : b ∈ encodable.decode2 β i), f b) = ⋃ (b : β), f b
theorem
encodable.Union_decode2_cases
{α : Type u_1}
{β : Type u_2}
[encodable β]
{f : β → set α}
{C : set α → Prop}
(H0 : C ∅)
(H1 : ∀ (b : β), C (f b))
{n : ℕ} :
C (⋃ (b : β) (H : b ∈ encodable.decode2 β n), f b)