nth_le_nth — Mathlib

English

Let p define an infinite subset of natural numbers. Then nth p k ≤ nth p n iff k ≤ n.

Русский

Пусть p задаёт бесконечное подмножество натура́льных чисел. Тогда nth p k ≤ nth p n эквивалентно k ≤ n.

LaTeX

$$$\\forall {p : \\mathbb{N} \\to \\mathbb{P}}, (\\{ n \\in \\mathbb{N} \\mid p(n) \\} \\text{ Infinite}) \\to \\forall {k n \\in \\mathbb{N}},\\; \\operatorname{nth} p k \\le \\operatorname{nth} p n \\iff k \\le n$$$

Lean4

theorem nth_le_nth (hf : (setOf p).Infinite) {k n} : nth p k ≤ nth p n ↔ k ≤ n :=
  (nth_strictMono hf).le_iff_le

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