English
Let r be a well-founded relation on α. For every nonempty subset s of α, there exists a ∈ s that is minimal with respect to r; i.e., ∀ x ∈ s, ¬ r x a.
Русский
Пусть r — хорошо основанное отношение на α. Для любой непустой подмножества s ⊆ α существует элемент a ∈ s, такой что для всех x ∈ s не выполняется r x a.
LaTeX
$$$\\text{WellFounded } r \\;\\to\\; \\forall s \\subseteq \\alpha,\\; s \\neq \\varnothing \\Rightarrow \\exists a\\in s,\\; \\forall x\\in s,\\; \\neg r\\,x\\,a$$$
Lean4
/-- If `r` is a well-founded relation, then any nonempty set has a minimal element
with respect to `r`. -/
theorem has_min {α} {r : α → α → Prop} (H : WellFounded r) (s : Set α) : s.Nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬r x a
| ⟨a, ha⟩ =>
show ∃ b ∈ s, ∀ x ∈ s, ¬r x b from
Acc.recOn (H.apply a)
(fun x _ IH => not_imp_not.1 fun hne hx => hne <| ⟨x, hx, fun y hy hyx => hne <| IH y hyx hy⟩) ha
