comap_comap — Mathlib

English

Precomposition is associative in the sense comap f (comap g x) = comap (g ∘ f) x for all x ∈ LocallyConstant(Y, Z).

Русский

Предкомпозиция ассоциативна: для любых x ∈ LocallyConstant(Y, Z) выполняется comap f (comap g x) = comap (g ∘ f) x.

LaTeX

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

Lean4

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

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