Theorems · Definition · algebraic topology

HSpace.hmulE

{X : Type u} →
  {inst : TopologicalSpace X} →
    [self : HSpace X] →
      (HSpace.hmul.comp ((ContinuousMap.id X).prodMk (ContinuousMap.const X HSpace.e))).HomotopyRel (ContinuousMap.id X)
        {HSpace.e}

Defined in

Mathlib.Topology.Homotopy.HSpaces

Cited by

0 results in Mathlib

Foundations

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

Assumes

HSpace