card_extend — Mathlib

English

In the extend construction, the new partition has exactly one more block than the original.

Русский

В конструировании расширения новое разбиение имеет ровно на один блок больше исходного.

LaTeX

$$$\#(P.extend hb hab hc).parts.card = \#P.parts.card + 1$$$

Lean4

theorem card_extend (P : Finpartition a) (b c : α) {hb : b ≠ ⊥} {hab : Disjoint a b} {hc : a ⊔ b = c} :
    #(P.extend hb hab hc).parts = #P.parts + 1 :=
  card_insert_of_notMem fun h ↦ hb <| hab.symm.eq_bot_of_le <| P.le h

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