lt_nth_iff_count_lt — Mathlib

English

For infinite p, a < count p b if and only if nth p a < b; i.e., the a-th index lies before the b-th threshold exactly when a-th count is below b.

Русский

Для бесконечного p выполняется эквивалентность: a < count p b ⇔ nth p a < b.

LaTeX

$$$$ a < \\mathrm{count}(p,b) \\iff \\mathrm{nth}(p,a) < b. $$$$

Lean4

theorem lt_nth_iff_count_lt (hp : (setOf p).Infinite) {a b : ℕ} : a < count p b ↔ nth p a < b :=
  (gc_count_nth hp).lt_iff_lt

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