comp_antitone

Mathlib.Order.Filter.Extr

URI: https://scilib.ai/kg/mathlib#IsMinOn.comp_antitone

English

If IsMinOn f s a and g is antitone, then g∘f is IsMaxOn on s at a.

Русский

Если IsMinOn f s a и g антимонотонна, то g∘f является IsMaxOn на s при a.

LaTeX

$$$\text{IsMinOn}(f,s,a) \rightarrow \text{Antitone}(g) \rightarrow \text{IsMaxOn}(g\circ f,s,a)$$$

Lean4

theorem comp_antitone (hf : IsMinOn f s a) {g : β → γ} (hg : Antitone g) : IsMaxOn (g ∘ f) s a :=
  IsMinFilter.comp_antitone hf hg

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

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

Разделы

Аффилиация

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