exists_max — Mathlib

English

For a finite nonempty α and a linear order β, any function f: α → β attains a maximum value; that is, there exists x0 ∈ α with f(x) ≤ f(x0) for all x ∈ α.

Русский

Для непустого конечного α и линейного порядка β функция f: α → β достигает максимума: существует x0 ∈ α такое, что f(x) ≤ f(x0) для всех x ∈ α.

LaTeX

$$$\\exists x_0 \\in \\alpha, \\forall x \\in \\alpha,\\ f(x) \\le f(x_0)$$$

Lean4

theorem exists_max [Finite α] [Nonempty α] [LinearOrder β] (f : α → β) : ∃ x₀ : α, ∀ x, f x ≤ f x₀ :=
  by
  cases nonempty_fintype α
  simpa using exists_max_image univ f univ_nonempty

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