exists_min — Mathlib

English

Let α be finite and nonempty, and f : α → β with β linearly ordered. There exists x₀ ∈ α such that f(x₀) ≤ f(x) for all x ∈ α.

Русский

Пусть α конечна и непустая, и f : α → β с линейным порядком. Существует x₀ ∈ α такое, что f(x₀) ≤ f(x) для всех x.

LaTeX

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

Lean4

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

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