exists_lower_bound_image — Mathlib

English

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

Русский

Пусть s ненулево конечно и есть отображение f; тогда существует a ∈ s такой, что f(a) ≤ f(b) для всех b ∈ s.

LaTeX

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

Lean4

theorem exists_lower_bound_image [Nonempty α] [LinearOrder β] (s : Set α) (f : α → β) (h : s.Finite) :
    ∃ a : α, ∀ b ∈ s, f a ≤ f b := by
  rcases s.eq_empty_or_nonempty with rfl | hs
  · exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩
  · rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩
    exact ⟨x₀, fun x hx => hx₀ x hx⟩

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