card_erase_eq_ite — Mathlib

English

The cardinality of s.erase a is given by a case distinction: #s − 1 if a ∈ s, otherwise #s.

Русский

Кардинал s.erase a задается различием по случаям: #s − 1, если a ∈ s, иначе #s.

LaTeX

$$$#(s.erase a) = \begin{cases} #s - 1, & a \in s \\ #s, & a \notin s \end{cases}$$$

Lean4

/-- If `a ∈ s` is known, see also `Finset.card_erase_of_mem` and `Finset.erase_eq_of_notMem`. -/
theorem card_erase_eq_ite : #(s.erase a) = if a ∈ s then #s - 1 else #s :=
  Multiset.card_erase_eq_ite

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