ncard_le_ncard_insert

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

For any a and any set s, s.ncard ≤ (insert a s).ncard.

Русский

Для любого a и множества s верно: s.ncard ≤ (insert a s).ncard.

LaTeX

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

Lean4

theorem ncard_le_ncard_insert (a : α) (s : Set α) : s.ncard ≤ (insert a s).ncard := by
  classical
  refine s.finite_or_infinite.elim (fun h ↦ ?_) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
  rw [ncard_insert_eq_ite h]; split_ifs <;> simp

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

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

Разделы

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

Аффилиация

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