empty — Mathlib

English

The empty Finpartition corresponds to the bottom element ⊥ in the lattice structure; it has no parts and trivial sup relations.

Русский

Пустое Finpartition соответствует нижнему элементу ⊥ в решётке; у него нет частей и тривиальные отношения над верхом.

LaTeX

$$$\\text{empty} : \\mathrm{Finpartition}(\\perp)$$$

Lean4

/-- The empty finpartition. -/
@[simps]
protected def empty : Finpartition (⊥ : α) where
  parts := ∅
  supIndep := supIndep_empty _
  sup_parts := Finset.sup_empty
  bot_notMem := notMem_empty ⊥

Похожие утверждения