exists_le_minimal — Mathlib

English

If s is PWO and a ∈ s, there exists b ≤ a that is a minimal element of s.

Русский

Если s — PWO и a ∈ s, существует b ≤ a, который минимален в s.

LaTeX

$$$(hs : s.IsPWO)(ha : a ∈ s) \\Rightarrow \\exists b \\le a, \\ Minimal(\\cdot \\in s) b$$$

Lean4

theorem exists_le_minimal {a} (hs : s.IsPWO) (ha : a ∈ s) : ∃ b ≤ a, Minimal (· ∈ s) b :=
  by
  let t : Set s := {x | x ≤ a}
  let h : t.Nonempty := ⟨⟨a, ha⟩, le_rfl⟩
  refine ⟨hs.wellFounded.min t h, hs.wellFounded.min_mem t h, (hs.wellFounded.min t h).2, fun y hy hle => ?_⟩
  by_contra hnle
  exact hs.wellFounded.not_lt_min t h (x := ⟨y, hy⟩) (hle.trans (hs.wellFounded.min_mem t h)) ⟨hle, hnle⟩

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