isLeast_nth_of_infinite — Mathlib

English

Let p: ℕ → Prop and setOf p infinite. Then for any n, IsLeast {i | p i ∧ ∀ k < n, nth p k < i} (nth p n) holds.

Русский

Пусть p: ℕ → ⊤ и {x | p x} бесконечно. Тогда для любого n элемент IsLeast множества {i | p i ∧ ∀ k < n, nth p k < i} равен nth p n.

LaTeX

$$$\\\\forall {p: \\\\mathbb{N} \\\\to \\\\mathsf{Prop}}\\\\ (setOf p)\\\\ Infinite \\\\Rightarrow \\\\ IsLeast \\\\{i \\\\mid p i \\\\land \\\\forall k < n,\\\\ nth p k < i\\\\}\\\\ (\\\\mathrm{nth}\\\\ p\\\\ n).$$$

Lean4

theorem isLeast_nth_of_infinite (hf : (setOf p).Infinite) (n : ℕ) :
    IsLeast {i | p i ∧ ∀ k < n, nth p k < i} (nth p n) :=
  isLeast_nth fun h => absurd h hf

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