comp_antitone

Mathlib.Order.Filter.Extr

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

English

If IsExtrOn f s a and g is antitone, then IsExtrOn (g ∘ f) s a.

Русский

Если IsExtrOn f s a и g антимонотонна, то IsExtrOn (g ∘ f) s a.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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