card_eraseNone_of_mem — Mathlib

English

If none ∈ s, then the erasure reduces the size by one: #s.eraseNone = #s − 1.

Русский

Если none ∈ s, тогда удаление none уменьшает размер на единицу: #s.eraseNone = #s − 1.

LaTeX

$$$\\text{none} \\in s \\Rightarrow \\#(s).\\text{eraseNone} = \\#s - 1$$$

Lean4

theorem card_eraseNone_of_mem {s : Finset (Option α)} (h : none ∈ s) : #s.eraseNone = #s - 1 := by
  classical rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]

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