count_mono_left — Mathlib

English

If p implies q pointwise, then count p n ≤ count q n for all n.

Русский

Если p(k) ⇒ q(k) для всех k, то count(p,n) ≤ count(q,n) для всех n.

LaTeX

$$$\forall n,\; \operatorname{count}(p,n) \le \operatorname{count}(q,n)$, при условии $\forall k,\ p(k) \Rightarrow q(k)$.$$

Lean4

theorem count_mono_left {n : ℕ} (hpq : ∀ k, p k → q k) : count p n ≤ count q n :=
  by
  simp only [count_eq_card_filter_range]
  exact card_le_card ((range n).monotone_filter_right hpq)

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