ncard_insert_le

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

The ncard of insert a s is at most s.ncard + 1.

Русский

ncard(insert a s) ≤ s.ncard + 1.

LaTeX

$$$ (insert\ a\ s).ncard \le s.ncard + 1 $$$

Lean4

theorem ncard_insert_le (a : α) (s : Set α) : (insert a s).ncard ≤ s.ncard + 1 :=
  by
  obtain hs | hs := s.finite_or_infinite
  · to_encard_tac; rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]; apply encard_insert_le
  rw [(hs.mono (subset_insert a s)).ncard]
  exact Nat.zero_le _

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

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

Разделы

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

Аффилиация

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