exists_upper_bound_image — Mathlib

English

Given a finite nonempty s and a function f, there exists a ∈ s such that f(b) ≤ f(a) for all b ∈ s.

Русский

Пусть s ненулево конечно; существует a ∈ s такой, что ∀ b ∈ s, f(b) ≤ f(a).

LaTeX

$$$\\exists a \\in s, \\forall b \\in s, f(b) \\le f(a)$$$

Lean4

theorem exists_upper_bound_image [Nonempty α] [LinearOrder β] (s : Set α) (f : α → β) (h : s.Finite) :
    ∃ a : α, ∀ b ∈ s, f b ≤ f a :=
  exists_lower_bound_image (β := βᵒᵈ) s f h

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