inter — Mathlib

English

If hf : IsLocalMinOn f s a, then for any t, IsLocalMinOn f (s ∩ t) a; the min-on-subset property holds under intersection.

Русский

Если 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 inter (hf : IsLocalMinOn f s a) (t) : IsLocalMinOn f (s ∩ t) a :=
  hf.on_subset inter_subset_left

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