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.supᵢ_decode₂ {α : Type u_1} {β : Type u_2} [inst : Encodable β] [inst : CompleteLattice α] (f : βα) :
(i, b, h, f b) = b, f b
theorem Encodable.unionᵢ_decode₂ {α : Type u_1} {β : Type u_2} [inst : Encodable β] (f : βSet α) :
(Set.unionᵢ fun i => Set.unionᵢ fun b => Set.unionᵢ fun h => f b) = Set.unionᵢ fun b => f b
theorem Encodable.unionᵢ_decode₂_cases {α : Type u_1} {β : Type u_2} [inst : Encodable β] {f : βSet α} {C : Set αProp} (H0 : C ) (H1 : (b : β) → C (f b)) {n : } :
C (Set.unionᵢ fun b => Set.unionᵢ fun h => f b)
theorem Encodable.unionᵢ_decode₂_disjoint_on {α : Type u_1} {β : Type u_2} [inst : Encodable β] {f : βSet α} (hd : Pairwise (Disjoint on f)) :
Pairwise (Disjoint on fun i => Set.unionᵢ fun b => Set.unionᵢ fun h => f b)