inf_eq_of_isMinOn

Mathlib.Order.Filter.Extr

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

English

Let a ∈ s and IsMinOn D s a. Then the infimum of D over s equals D(a).

Русский

Пусть a ∈ s и IsMinOn D s a. Тогда инфимум D над s равен D(a).

LaTeX

$$$(a \\in s) \\land IsMinOn D s a \\Rightarrow s.inf D = D(a)$$$

Lean4

theorem inf_eq_of_isMinOn {a : α} (hmem : a ∈ s) (hmax : IsMinOn D s a) : s.inf D = D a :=
  sup_eq_of_isMaxOn (α := αᵒᵈ) (β := βᵒᵈ) hmem hmax.dual

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

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

Разделы

Аффилиация

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