card_insert — Mathlib

English

For a finite set s and a not-in-s element a, the cardinality of s ∪ {a} equals |s| + 1.

Русский

Для конечного множества s и элемента a, не принадлежащего s, кардинальность s ∪ {a} равна |s| + 1.

LaTeX

$$$ |s \\cup \\{a\\}| = |s| + 1 \\quad (a \\notin s) $$$

Lean4

@[simp]
theorem card_insert {a : α} (s : Set α) [Fintype s] (h : a ∉ s) {d : Fintype (insert a s : Set α)} :
    @Fintype.card _ d = Fintype.card s + 1 := by rw [← card_fintypeInsertOfNotMem s h]; congr!

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