count_le_setENCard

Mathlib.SetTheory.Cardinal.NatCount

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

← MathLib Explorer

English

The count of p up to n is bounded by the encard of the set {k | p k}.

Русский

Счёт p до n не превышает encard множества {k | p k}.

LaTeX

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

Lean4

theorem count_le_setENCard : count p n ≤ Set.encard {k | p k} :=
  by
  simp only [Set.encard, ENat.card, Set.coe_setOf, Cardinal.natCast_le_toENat_iff]
  exact Nat.count_le_cardinal n

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

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

Разделы

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

Аффилиация

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