isMinOn_univ_iff — Mathlib

English

For any function f and a, IsMinOn f univ a holds exactly when f(a) ≤ f(x) for all x in the domain.

Русский

Для любой функции f и элемента a справедливо IsMinOn f univ a тогда и только тогда, когда f(a) ≤ f(x) для всех x.

LaTeX

$$$IsMinOn\ f\ Set.univ\ a \iff \forall x,\ f(a) \le f(x)$$$

Lean4

theorem isMinOn_univ_iff : IsMinOn f univ a ↔ ∀ x, f a ≤ f x :=
  univ_subset_iff.trans eq_univ_iff_forall

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