on_subset — Mathlib

English

For IsLocalExtr f a, the elimination principle states that from IsLocalMin f a and IsLocalMax f a, one can deduce p as in the IsLocalExtr.elim theorem.

Русский

Для IsLocalExtr f a принцип устранения говорит, что из IsLocalMin f a и IsLocalMax f a можно вывести p согласно теореме IsLocalExtr.elim.

LaTeX

$$$IsLocalExtr f a \rightarrow (IsLocalMin f a \rightarrow p) \rightarrow (IsLocalMax f a \rightarrow p) \rightarrow p$$$

Lean4

theorem on_subset {t : Set α} (hf : IsLocalMinOn f t a) (h : s ⊆ t) : IsLocalMinOn f s a :=
  hf.filter_mono <| nhdsWithin_mono a h

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