encard_insert_of_notMem

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.encard_insert_of_notMem

← MathLib Explorer

English

If a ∉ s, then encard(insert a s) = s.encard + 1.

Русский

Если a не принадлежит s, то encard(insert a s) = s.encard + 1.

LaTeX

$$$ (\text{insert } a\ s).encard = s.encard + 1 $$$

Lean4

theorem encard_insert_of_notMem {a : α} (has : a ∉ s) : (insert a s).encard = s.encard + 1 := by
  rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]

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

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

Разделы

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

Аффилиация

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