inter — Mathlib

English

If hf : IsLocalMaxOn f s a, then IsLocalMaxOn f (s ∩ t) a for any t; the local maximum property is stable under intersection.

Русский

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

LaTeX

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

Lean4

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

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