English
If α is a complete lattice and P is a partition of s whose parts generate s and do not contain the bottom element, then the partition obtained by removing ⊥ from the set of parts is again a partition of s.
Русский
Пусть α — полная решётка и P — разбиение s так, что объединение частей даёт s и ⊥ не является одной из частей; тогда разбиение P \ {⊥} снова является разбиением s.
LaTeX
$$$P \\setminus\\{\\perp\\}\\text{ is a partition of } s \\text{ provided } sSupIndep(P) \\text{ and } sSup(P)=s \\text{ and } \\perp \\notin P$.$$
Lean4
/-- A constructor for `Partition s` that removes `⊥` from the set of parts. -/
@[simps]
def removeBot (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : Partition s
where
parts := P \ {⊥}
sSupIndep' := indep.mono diff_subset
bot_notMem' := by simp
sSup_eq' := by simp [← sSup_eq]
