English
Let α be a well-founded ordered set with relation r. Then the set of records S = {a in α | for all b, if r b a then b < a} is cofinal in α.
Русский
Пусть α упорядочено по хорошо основанному отношению r. Тогда множество записей S = {a в α | для всех b, если r b a, то b < a} кофинально относительно α.
LaTeX
$$$\\\\mathrm{IsCofinal} \\left( \\{a \\\\in \\\\alpha \\\\mid \\\\forall b,\ \ r\\\\ b \\\\ a \\\\Rightarrow \\\\ b < \\\\ a\\\\} \\right)$$$
Lean4
/-- The set of "records" (the smallest inputs yielding the highest values) with respect to a
well-ordering of `α` is a cofinal set. -/
theorem isCofinal_setOf_imp_lt (r : α → α → Prop) [h : IsWellFounded α r] : IsCofinal {a | ∀ b, r b a → b < a} :=
by
intro a
obtain ⟨b, hb, hb'⟩ := h.wf.has_min (Set.Ici a) Set.nonempty_Ici
refine ⟨b, fun c hc ↦ ?_, hb⟩
by_contra! hc'
exact hb' c (hb.trans hc') hc
