count_le_iff_le_nth — Mathlib

English

Under the infinite predicate assumption, the count_le_iff_le_nth equivalence holds: count p a ≤ b iff a ≤ nth p b, reflecting the Galois connection between count and nth.

Русский

При бесконечном предикате выполняется эквивалентность: count p a ≤ b если и только если a ≤ nth p b.

LaTeX

$$$$ \\forall a,b:\\mathbb{N}, \\; (\\text{Infinite }(\\{n:\\, p(n)\\})) \\Rightarrow \\big( \\mathrm{count}(p,a) \\le b \\iff a \\le \\mathrm{nth}(p,b) \\big). $$$$

Lean4

theorem count_le_iff_le_nth (hp : (setOf p).Infinite) {a b : ℕ} : count p a ≤ b ↔ a ≤ nth p b :=
  gc_count_nth hp _ _

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