exists_maximal — Mathlib

English

Let s be a finite subset of α with a preorder. If s is nonempty, then there exists x ∈ s such that x is maximal in s.

Русский

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

LaTeX

$$$s\text{ finite and } s \neq \emptyset \Rightarrow \exists x \in s,\ \forall y \in s,\ x \ge y.$$$

Lean4

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

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