wellFounded_iff_has_min — Mathlib

English

A relation r is well-founded if and only if every nonempty subset s has a minimal element with respect to r.

Русский

Отношение r является хорошо основанным тогда и только тогда, когда любым непустым подмножеством s соответствует минимальный элемент по отношению r.

LaTeX

$$$\\text{WellFounded } r \\iff \\forall s,\\; s \\neq \\varnothing \\Rightarrow \\exists m\\in s,\\; \\forall x\\in s,\\; \\neg r\\,x\\,m$$$

Lean4

theorem wellFounded_iff_has_min {r : α → α → Prop} :
    WellFounded r ↔ ∀ s : Set α, s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m :=
  by
  refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩
  by_contra hx
  obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩
  refine hm ⟨_, fun y hy => ?_⟩
  by_contra hy'
  exact hm' y hy' hy

Похожие утверждения