elim — Mathlib

English

IsLocalExtrOn f s a is the local extremum of f on s at a, i.e., either a local minimum or local maximum on s at a.

Русский

IsLocalExtrOn f s a есть локальный экстремум функции f на множестве s в точке a, то есть либо локальный минимум, либо локальный максимум на s в a.

LaTeX

$$$IsLocalExtrOn(f,s,a)\;:=\;IsExtrFilter(f,\,\mathcal{N}_s(a),\,a)$$$

Lean4

theorem elim {p : Prop} : IsLocalExtrOn f s a → (IsLocalMinOn f s a → p) → (IsLocalMaxOn f s a → p) → p :=
  Or.elim

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