comp_monotone_left

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#Antivary.comp_monotone_left

English

If Antivary f g and f' is monotone, then Antivary (f' ∘ f) g.

Русский

Если Antivary f g и f' монотонна, то Antivary (f' ∘ f) g.

LaTeX

$$$\\operatorname{Antivary}(f,g) \\rightarrow \\operatorname{Monotone}(f') \\rightarrow \\operatorname{Antivary}(f' \\circ f, g)$$$

Lean4

theorem comp_monotone_left (h : Antivary f g) (hf : Monotone f') : Antivary (f' ∘ f) g := fun _ _ hij => hf <| h hij

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

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

Разделы

Аффилиация

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