exists_maximal — Mathlib

English

Let α be a preorder and s ⊆ α a nonempty finite set. Then there exists x ∈ s which is maximal in s, i.e., no element of s is strictly greater than x.

Русский

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

LaTeX

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

Lean4

theorem exists_maximal (hs : s.Nonempty) : ∃ i, Maximal (· ∈ s) i :=
  s.exists_maximalFor id hs

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