exists_minimal — 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 minimal 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 \le y.$$$

Lean4

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

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