exists_min_image — Mathlib

English

Dual to exists_max_image: there exists an element x ∈ s minimizing f(x) among s, i.e., f(x) ≤ f(y) for all y ∈ s.

Русский

Двойственно существует минимальный образ: существует элемент x ∈ s, такой что f(x) минимален по отношению к всем элементам s.

LaTeX

$$$\\exists x \\in s, \\forall y \\in s, f(x) \\le f(y)$$$

Lean4

theorem exists_min_image (s : Finset β) (f : β → α) (h : s.Nonempty) : ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x' :=
  @exists_max_image αᵒᵈ β _ s f h

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