count_le

Mathlib.Data.Nat.Count

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

English

For any predicate p, count p n is at most n.

Русский

Для любого предиката p число count p n не превосходит n.

LaTeX

$$$$\operatorname{count}(p,n) \le n.$$$$

Lean4

theorem count_le {n : ℕ} : count p n ≤ n := by
  rw [count_eq_card_filter_range]
  exact (card_filter_le _ _).trans_eq (card_range _)

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

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

Разделы

Аффилиация

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