mathlib3 documentation

logic.encodable.lattice

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)) :
pairwise (disjoint on λ (i : ), (b : β) (H : b encodable.decode₂ β i), f b)