card_erase_add_one

Mathlib.Data.Finset.Card

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

English

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

Русский

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

LaTeX

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

Lean4

theorem card_erase_add_one : a ∈ s → #(s.erase a) + 1 = #s :=
  Multiset.card_erase_add_one

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

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

Разделы

Аффилиация

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