polar_comp — Mathlib

English

The polar map commutes with composition with a function: polar (g ∘ f) x y = g(polar f x y).

Русский

Полярная карта коммутирует с композициями: polar (g ∘ f) x y = g(polar f x y).

LaTeX

$$$$ polar (g \\circ f) \\; x \\; y = g( polar f \\; x \\; y ). $$$$

Lean4

theorem polar_comp {F : Type*} [AddCommGroup S] [FunLike F N S] [AddMonoidHomClass F N S] (f : M → N) (g : F)
    (x y : M) : polar (g ∘ f) x y = g (polar f x y) := by simp only [polar, Function.comp_apply, map_sub]

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