Documentation

Mathlib.Logic.Encodable.Lattice

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