elim — Mathlib

English

For any proposition p, if IsLocalExtrOn f s a holds, then from IsLocalMinOn f s a → p and IsLocalMaxOn f s a → p, we may conclude p.

Русский

Для любого утверждения p, если IsLocalExtrOn f s a выполняется, то из IsLocalMinOn f s a → p и IsLocalMaxOn f s a → p следует вывод p.

LaTeX

$$$IsLocalExtrOn f s a \rightarrow (IsLocalMinOn f s a \rightarrow p) \rightarrow (IsLocalMaxOn f s a \rightarrow p) \rightarrow p$$$

Lean4

theorem elim {p : Prop} : IsLocalExtr f a → (IsLocalMin f a → p) → (IsLocalMax f a → p) → p :=
  Or.elim

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