English
If r is a well-founded relation and s is a nonempty subset, then the minimal element of s with respect to r lies in s.
Русский
Пусть r — хорошо основанное отношение и s — непустое подмножество; минимальный по r элемент s принадлежит s.
LaTeX
$$$\\forall \\alpha\\; \\forall r:\\alpha\\to\\alpha\\to\\mathrm{Prop},\\; (\\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
theorem min_mem {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) : H.min s h ∈ s :=
let ⟨h, _⟩ := Classical.choose_spec (H.has_min s h)
h
