English
Extending a finpartition by adding a new element increases the number of parts by one.
Русский
Расширение финразбиения добавлением нового элемента увеличивает число блоков на единицу.
LaTeX
$$$\#(P.extend hb hab hc).parts = \#P.parts + 1$$$
Lean4
/-- Adds `b` to a finpartition of `a` to make a finpartition of `a ⊔ b`. -/
@[simps]
def extend (P : Finpartition a) (hb : b ≠ ⊥) (hab : Disjoint a b) (hc : a ⊔ b = c) : Finpartition c
where
parts := insert b P.parts
supIndep := by
rw [supIndep_iff_pairwiseDisjoint, coe_insert]
exact P.disjoint.insert fun d hd _ ↦ hab.symm.mono_right <| P.le hd
sup_parts := by rwa [sup_insert, P.sup_parts, id, _root_.sup_comm]
bot_notMem h := (mem_insert.1 h).elim hb.symm P.bot_notMem
