inter — Mathlib

English

IsLocalExtrOn f s a implies IsLocalExtrOn f t a for appropriate t; local extremum on a set transfers to a sub-collection.

Русский

IsLocalExtrOn f s a влечет IsLocalExtrOn f t a для подходящих t; локальный экстремум на множестве переносится на подколлекцию.

LaTeX

$$$IsLocalExtrOn f s a \rightarrow \forall t, IsLocalExtrOn f t a$$$

Lean4

theorem inter (hf : IsLocalExtrOn f s a) (t) : IsLocalExtrOn f (s ∩ t) a :=
  hf.on_subset inter_subset_left

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