English
Let p: ℕ → Prop. Then nth p n is the least element i such that p i holds and i is larger than all previous nth values; i.e., i ≥ nth p k for all k < n and p i holds.
Русский
Пусть p: ℕ → ⊤. Тогда x = nth p n является наименьшим элементом среди тех i, для которых p i истинно и которые превосходят все предшествующие nth p k.
LaTeX
$$$\\\\text{IsLeast}\\\\{i \\\\mid p i \\\\land \\\\forall k < n,\\\\ nth p k < i\\\\}\\\\ (\\\\mathrm{nth}\\\\ p\\\\ n).$$$
Lean4
theorem isLeast_nth {n} (h : ∀ hf : (setOf p).Finite, n < #hf.toFinset) :
IsLeast {i | p i ∧ ∀ k < n, nth p k < i} (nth p n) :=
⟨⟨nth_mem n h, fun _k hk => nth_lt_nth' hk h⟩, fun _x hx =>
let ⟨k, hk, hkx⟩ := exists_lt_card_nth_eq hx.1
(lt_or_ge k n).elim (fun hlt => absurd hkx (hx.2 _ hlt).ne) fun hle => hkx ▸ nth_le_nth' hle hk⟩
