nth_of_forall — Mathlib

English

If a predicate p holds for all numbers up to n (i.e., ∀ m ≤ n, p(m) holds), then the n-th true value of p equals n.

Русский

Если предикат p истинен на всём Interval [0,n], то n-й истинный элемент p равен n.

LaTeX

$$$$ \\forall n:\\mathbb{N}, \\; (\\forall m \\le n, p(m)) \\Rightarrow \\mathrm{nth}(p,n) = n. $$$$

Lean4

theorem nth_of_forall {n : ℕ} (hp : ∀ n' ≤ n, p n') : nth p n = n := by
  classical nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]

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