isMaxOn_univ_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isMaxOn_univ_iff : IsMaxOn f univ a ↔ ∀ x, f x ≤ f a :=
  univ_subset_iff.trans eq_univ_iff_forall

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