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