Theorems · Definition · general topology

ContinuousMap.unitsLift

{X : Type u_1} →
  {M : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : Monoid M] → [inst_2 : TopologicalSpace M] → [inst_3 : ContinuousMul M] → C(X, Mˣ) ≃ C(X, M)ˣ

Equivalence between continuous maps into the units of a monoid with continuous multiplication and the units of the monoid of continuous maps.

Defined in

Mathlib.Topology.ContinuousMap.Units

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMonoidTopologicalSpaceContinuousMul