on_subset — Mathlib

English

If hf is IsLocalMinOn f s a, then for any t, IsLocalMinOn f (s ∩ t) a; i.e., the local minimum property persists on intersections.

Русский

Если hf — IsLocalMinOn f s a, то для любого t топологически сохраняется IsLocalMinOn f (s ∩ t) a; свойство локального минимума сохраняется на пересечении.

LaTeX

$$$IsLocalMinOn\ f\ s\ a \rightarrow \forall t, IsLocalMinOn f (s \cap t) a$$$

Lean4

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

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