Theorems · Definition · general topology

AddCircle.openPartialHomeomorphCoe

{𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    (p : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsOrderedAddMonoid 𝕜] →
          [hp : Fact (0 < p)] →
            𝕜 →
              [Archimedean 𝕜] →
                [inst_4 : TopologicalSpace 𝕜] →
                  [OrderTopology 𝕜] →
                    [DiscreteTopology ↥(AddSubgroup.zmultiples p)] → OpenPartialHomeomorph 𝕜 (AddCircle p)

The quotient map 𝕜 → AddCircle p as an open partial homeomorphism.

Defined in

Mathlib.Topology.Instances.AddCircle.Defs

Cited by

4 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidFactArchimedeanTopologicalSpaceOrderTopologyDiscreteTopology