mathlib documentation

data.equiv.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_decode2 {α : Type u_1} {β : Type u_2} [encodable β] [complete_lattice α] (f : β → α) :
(⨆ (i : ) (b : β) (H : b encodable.decode2 β i), f b) = ⨆ (b : β), f b

theorem encodable.Union_decode2 {α : Type u_1} {β : Type u_2} [encodable β] (f : β → set α) :
(⋃ (i : ) (b : β) (H : b encodable.decode2 β i), f b) = ⋃ (b : β), f b

theorem encodable.Union_decode2_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.decode2 β n), f b)

theorem encodable.Union_decode2_disjoint_on {α : Type u_1} {β : Type u_2} [encodable β] {f : β → set α} :
pairwise (disjoint on f)pairwise (disjoint on λ (i : ), ⋃ (b : β) (H : b encodable.decode2 β i), f b)

theorem finset.nonempty_encodable {α : Type u_1} (t : finset α) :
nonempty (encodable {i // i t})