English
The bottom finpartition (the partition that has only the bottom element as a part) is equipartition.
Русский
Нижнее Finpartition — это разбиение, содержащее только нижний элемент как одну часть, и оно является равномерным.
LaTeX
$$$\\mathrm{IsEquipartition}(\\mathrm{instBotFinset}.bot)$$$
Lean4
/-- A `Finpartition` constructor which does not insist on `⊥` not being a part. -/
@[simps]
def ofErase [DecidableEq α] {a : α} (parts : Finset α) (sup_indep : parts.SupIndep id) (sup_parts : parts.sup id = a) :
Finpartition a where
parts := parts.erase ⊥
supIndep := sup_indep.subset (erase_subset _ _)
sup_parts := (sup_erase_bot _).trans sup_parts
bot_notMem := notMem_erase _ _
