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_decode₂
{α : Type u_1}
{β : Type u_2}
[encodable β]
[complete_lattice α]
(f : β → α) :
(⨆ (i : ℕ) (b : β) (H : b ∈ encodable.decode₂ β i), f b) = ⨆ (b : β), f b
theorem
encodable.Union_decode₂
{α : Type u_1}
{β : Type u_2}
[encodable β]
(f : β → set α) :
(⋃ (i : ℕ) (b : β) (H : b ∈ encodable.decode₂ β i), f b) = ⋃ (b : β), f b
theorem
encodable.Union_decode₂_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.decode₂ β n), f b)