English
Let hf be a finite set {x | p x}, with n < |hf.toFinset|. Then IsLeast of {i | p i ∧ ∀ k < n, nth p k < i} at i = nth p n.
Русский
Пусть hf — конечное множество {x | p x}, и если n < |hf.toFinset}, тогда IsLeast устанавливается для i = nth p n.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ (hf:\\\\{x:\\\\mathbb{N}\\\\mid p x\\\\}\\\\Finite)\\\\ (hn : n < #hf.toFinset) \\\\Rightarrow \\\\ IsLeast \\\\{i \\\\mid p i \\\\land \\\\forall k < n,\\\\ nth p k < i\\\\}\\\\ (\\\\mathrm{nth}\\\\ p\\\\ n).$$$
Lean4
theorem isLeast_nth_of_lt_card {n : ℕ} (hf : (setOf p).Finite) (hn : n < #hf.toFinset) :
IsLeast {i | p i ∧ ∀ k < n, nth p k < i} (nth p n) :=
isLeast_nth fun _ => hn
