mathlib documentation

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 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)
theorem finset.nonempty_encodable {α : Type u_1} (t : finset α) :
nonempty (encodable {i // i t})