exists_minimal — Mathlib

English

Let α be a preorder and s ⊆ α a nonempty finite set. Then there exists x ∈ s such that x is minimal in s, i.e., no element of s is strictly smaller than x.

Русский

Пусть α — предордер, и s ⊆ α — непустое конечное множество. Тогда существует элемент x ∈ s, минимальный в s, то есть не существует y ∈ s с y < x.

LaTeX

$$$\exists x \in s,\forall y \in s,\ x \le y.$$$

Lean4

theorem exists_minimal (hs : s.Nonempty) : ∃ i, Minimal (· ∈ s) i :=
  s.exists_minimalFor id hs

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