max_of_nonempty — Mathlib

English

Let s be a nonempty finite subset of a linearly ordered set. Then the maximum of s is attained by some element of s.

Русский

Пусть s — непустое конечное множество в линейно упорядоченном множестве. Тогда максимум s достигается элементом s.

LaTeX

$$$\exists a \in s, \max s = a$$$

Lean4

theorem max_of_nonempty {s : Finset α} (h : s.Nonempty) : ∃ a : α, s.max = a :=
  let ⟨_, h⟩ := h
  max_of_mem h

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