count_le_setNCard

Mathlib.SetTheory.Cardinal.NatCount

URI: https://scilib.ai/kg/mathlib#Nat.count_le_setNCard

← MathLib Explorer

English

If {k | p k} is finite, then count p n ≤ Set.ncard {k | p k}.

Русский

Если множество {k | p k} конечное, то count p n ≤ Set.ncard {k | p k}.

LaTeX

$$count p n ≤ Set.ncard {k | p k}$$

Lean4

theorem count_le_setNCard (h : {k | p k}.Finite) : count p n ≤ Set.ncard {k | p k} :=
  by
  rw [Set.ncard_def, ← ENat.coe_le_coe, ENat.coe_toNat (by simpa)]
  exact count_le_setENCard n

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

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

Разделы

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

Аффилиация

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