exists_minimal — Mathlib

English

If s is PWO and nonempty, there exists a minimal element of s.

Русский

Если s частично хорошо упорядочено и непусто, существует минимальный элемент s.

LaTeX

$$$\\operatorname{IsPWO}(s) \\land s \\neq \\emptyset \\Rightarrow \\exists a, \\ Minimal(\\cdot \\in s) a$$$

Lean4

theorem exists_minimal (h : s.IsPWO) (hs : s.Nonempty) : ∃ a, Minimal (· ∈ s) a :=
  by
  rcases hs with ⟨a, ha⟩
  obtain ⟨b, _, hb⟩ := h.exists_le_minimal ha
  exact ⟨b, hb⟩

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