card_insert_eq_ite — Mathlib

English

For any finite set s and element a, the cardinality of insert a into s equals #s if a ∈ s, and equals #s + 1 otherwise.

Русский

Для любого конечного множества s и элемента a кардинал множества insert a s равен |s|, если a ∈ s, иначе |s| + 1.

LaTeX

$$$\#(\mathrm{insert}\ a\ s) = \begin{cases} \#s, & a \in s \\ \#s + 1, & a \notin s \end{cases}$$$

Lean4

/-- If `a ∈ s` is known, see also `Finset.card_insert_of_mem` and `Finset.card_insert_of_notMem`.
-/
theorem card_insert_eq_ite : #(insert a s) = if a ∈ s then #s else #s + 1 := by grind

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