card_eraseNone_of_not_mem — Mathlib

English

Let S be a finite Finset of elements of the type Option α, and suppose None is not a member of S. Then removing None does not change the cardinality: |eraseNone(S)| = |S|.

Русский

Пусть S — конечное множество элементов типа Option α, и None не принадлежит S. Тогда удаление None не изменяет кардиналость: |eraseNone(S)| = |S|.

LaTeX

$$$\text{If } \text{None} \notin S, \quad |\text{eraseNone}(S)| = |S|.$$$

Lean4

theorem card_eraseNone_of_not_mem {s : Finset (Option α)} (h : none ∉ s) : #s.eraseNone = #s := by
  classical rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]

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