English
Let r be a well-founded relation and s a nonempty set. If m is the minimal element of s with respect to r, then no element of s is strictly related to m by r; i.e., ∀ x ∈ s, ¬ r x m.
Русский
Пусть r — хорошо основанное отношение и s — непустое множество. Если m — минимальный элемент s по отношению r, то для любого x∈s неверно, что r x m.
LaTeX
$$$\\forall \\alpha\\; \\forall r:\\alpha\\to\\alpha\\to\\mathrm{Prop},\\; (\\text{WellFounded } r)\\to (\\forall s\\subseteq \\alpha,\\; s\\neq \\varnothing\\Rightarrow \\forall x\\in s,\\; \\neg r\\,x\\,(\\text{min}_r s))$$$
Lean4
theorem not_lt_min {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) {x} (hx : x ∈ s) :
¬r x (H.min s h) :=
let ⟨_, h'⟩ := Classical.choose_spec (H.has_min s h)
h' _ hx
