English
For p: ℕ → Prop and n ∈ ℕ, nth p n equals the sInf of the set {x | p x ∧ ∀ k < n, nth p k < x}.
Русский
Для p: ℕ → ⊤ и n ∈ ℕ, nth p n равно sInf множества {x | p x ∧ ∀ k < n, nth p k < x}.
LaTeX
$$$\\\\forall p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop},\\\\ \\nth p\\\\ n=\\\\,sInf\\\\{x \\\\mid p x \\\\\land \\\\forall k < n,\\\\ nth p k < x\\\\}.$$$
Lean4
/-- An alternative recursive definition of `Nat.nth`: `Nat.nth s n` is the infimum of `x ∈ s` such
that `Nat.nth s k < x` for all `k < n`, if this set is nonempty. We do not assume that the set is
nonempty because we use the same "garbage value" `0` both for `sInf` on `ℕ` and for `Nat.nth s n`
for `n ≥ #s`. -/
theorem nth_eq_sInf (p : ℕ → Prop) (n : ℕ) : nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x} :=
by
by_cases hn : ∀ hf : (setOf p).Finite, n < #hf.toFinset
· exact (isLeast_nth hn).csInf_eq.symm
· push_neg at hn
rcases hn with ⟨hf, hn⟩
rw [nth_of_card_le _ hn]
refine ((congr_arg sInf <| Set.eq_empty_of_forall_notMem fun k hk => ?_).trans sInf_empty).symm
rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
exact (hk.2 _ ((hlt hf).trans_le hn)).false
