Theorems · Theorem · algebraic topology

ContinuousMap.HomotopyEquiv.trans_apply

∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) (a : X),
  (h₁.trans h₂).toFun a = h₂.toFun (h₁.toFun a)

Defined in

Mathlib.Topology.Homotopy.Equiv

Cited by

0 results in Mathlib

Foundations

Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace