comp_right

Mathlib.Order.Monotone.Monovary

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

English

If Antivary f g holds, then for any k, Antivary (f ∘ k) (g ∘ k).

Русский

Если Antivary f g выполняется, то для любого k выполняется Antivary (f ∘ k) (g ∘ k).

LaTeX

$$$\\operatorname{Antivary}(f,g) \\Rightarrow \\forall k:\\\\iota' \\to \\\\iota, \\operatorname{Antivary}(f \\circ k, g \\circ k)$$$

Lean4

theorem comp_right (h : Antivary f g) (k : ι' → ι) : Antivary (f ∘ k) (g ∘ k) := fun _ _ hij => h hij

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

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

Разделы

Аффилиация

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