comap_comp — Mathlib

English

Precomposition along a composed map equals the composition of precompositions: comap (g ∘ f) = comap f ∘ comap g.

Русский

Предкомпозиция по композиции равна композиции предкомпозиций: comap (g ∘ f) = comap f ∘ comap g.

LaTeX

$$$ comap\\ (g \\circ f) = comap\\ f \\circ comap\\ g $$$

Lean4

theorem comap_comp {W : Type*} [TopologicalSpace W] (f : C(W, X)) (g : C(X, Y)) :
    comap (Z := Z) (g.comp f) = comap f ∘ comap g :=
  rfl

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