isLocalMinOn_univ_iff

Mathlib.Topology.Order.LocalExtr

URI: https://scilib.ai/kg/mathlib#isLocalMinOn_univ_iff

English

If hf : IsLocalMinOn f s a and hs : s ∈ 𝓝 a, then IsLocalMin f a.

Русский

Если hf : IsLocalMinOn f s a и hs : s ∈ 𝓝 a, тогда IsLocalMin f a.

LaTeX

$$$IsLocalMinOn\ f\ s\ a \rightarrow (s \in 𝓝 a) \rightarrow IsLocalMin f a$$$

Lean4

theorem isLocalMinOn_univ_iff : IsLocalMinOn f univ a ↔ IsLocalMin f a := by
  simp only [IsLocalMinOn, IsLocalMin, nhdsWithin_univ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru