card_fintypeInsertOfNotMem — Mathlib

English

If a is not in s, then the cardinality increases by one when inserting a into s.

Русский

Если a не принадлежит s, то при вставке a в s кардинальность увеличивается на единицу.

LaTeX

$$$ \\text{card} (\\text{insert } a\, s) = \\text{card } s + 1 \\quad (a \\notin s) $$$

Lean4

theorem card_fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) :
    @Fintype.card _ (fintypeInsertOfNotMem s h) = Fintype.card s + 1 := by
  simp [fintypeInsertOfNotMem, Fintype.card_ofFinset]

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