English
Let f: α → β, s ⊆ α, and a ∈ α. If a is an extreme point of f on s (i.e., either a minimizes f on s or a maximizes f on s), then for any proposition p, if p follows from a being a minimum and also from a being a maximum, then p.
Русский
Пусть f: α → β, s ⊆ α и a ∈ α. Если a является экстремумом f на s (то есть либо минимизирует f на s, либо максимизирует f на s), тогда для любого p из пропозиций верно: если p следует из того, что a минимально, и также следует из того, что a максимален, то p.
LaTeX
$$$IsExtrOn(f,s,a) \to (IsMinOn(f,s,a) \to p) \to (IsMaxOn(f,s,a) \to p) \to p$$$
Lean4
theorem elim {p : Prop} : IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → p :=
Or.elim
