English
Let s be a finite set. The bottom element of the partition lattice on s is the partition into singleton blocks: each element of s forms its own block.
Русский
Пусть s — конечное множество. Нижний элемент решетки разбиений на s есть разбиение на единичные множества: каждое элемент s образует собственную блок.
LaTeX
$$$ (\\perp_{Finpartition(s)}).\\text{parts} = s.\\\\map(\\\\text{singleton}) $$$
Lean4
/-- `⊥` is the partition in singletons, aka discrete partition. -/
instance (s : Finset α) : Bot (Finpartition s) :=
⟨{ parts := s.map ⟨singleton, singleton_injective⟩
supIndep :=
Set.PairwiseDisjoint.supIndep <| by
rw [Finset.coe_map]
exact Finset.pairwiseDisjoint_range_singleton.subset (Set.image_subset_range _ _)
sup_parts := by rw [sup_map, id_comp, Embedding.coeFn_mk, Finset.sup_singleton_eq_self]
bot_notMem := by simp }⟩
