Lattice operations on encodable types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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)

theorem encodable.Union_decode₂_disjoint_on {α : Type u_1} {β : Type u_2} [encodable β] {f : β → set α} (hd : pairwise (disjoint on f)) :