card_erase_of_mem

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.card_erase_of_mem

← MathLib Explorer

English

If a ∈ s, then #(s.erase a) = #s − 1.

Русский

Если a ∈ s, то #(s.erase a) = #s − 1.

LaTeX

$$$a \in s \Rightarrow #(s.erase a) = #s - 1$$$

Lean4

/-- $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. -/
@[simp, grind =]
theorem card_erase_of_mem : a ∈ s → #(s.erase a) = #s - 1 :=
  Multiset.card_erase_of_mem

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru