count_le_cardinal — Mathlib

English

For any predicate p on natural numbers, the cardinality of the count of numbers ≤ n is bounded by the cardinality of {k | p k}.

Русский

Для любого p на натуралах кардинал количества чисел ≤ n ограничен кардиналом множества {k | p k}.

LaTeX

$$(count p n : Cardinal) ≤ Cardinal.mk {k | p k}$$

Lean4

theorem count_le_cardinal : (count p n : Cardinal) ≤ Cardinal.mk {k | p k} :=
  by
  rw [count_eq_card_fintype, ← Cardinal.mk_fintype]
  exact Cardinal.mk_subtype_mono fun x hx ↦ hx.2

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