English
Let α be a lattice with a bottom element ⊥. If a ∈ α satisfies a ≠ ⊥, there exists a finpartition of a consisting of a single block {a}. This partition has the standard indiscrete (one-block) structure: the only block is a itself, its supremum equals a, and the bottom element is not contained in the block.
Русский
Пусть α — решетка с нулём ⊥. Пусть a ∈ α и a ≠ ⊥. Существует конечное разбиение a, состоящее из одного блока {a}. Это одночастное разбиение: единственный блок равен a, наибольший элемент разбиения равен a, и нижняя грань не лежит в блоке.
LaTeX
$$$\text{indiscrete}(a) : \text{Finpartition}(a)$ with parts = \{a\}, supIndep = supIndep\_singleton( a ), sup\_parts = \text{Finset}.sup\_singleton, bot\_notMem: a ≠ ⊥$$
Lean4
/-- The finpartition in one part, aka indiscrete finpartition. -/
@[simps]
def indiscrete (ha : a ≠ ⊥) : Finpartition a where
parts := { a }
supIndep := supIndep_singleton _ _
sup_parts := Finset.sup_singleton
bot_notMem h := ha (mem_singleton.1 h).symm
