Theorems · Theorem · general topology
AddCircle.openPartialHomeomorphCoe_apply
∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
[hp : Fact (0 < p)] (a : 𝕜) [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [inst_5 : OrderTopology 𝕜]
[inst_6 : DiscreteTopology ↥(AddSubgroup.zmultiples p)] (a_1 : 𝕜),
↑(AddCircle.openPartialHomeomorphCoe p a) a_1 = ↑a_1- Cited by
- 0 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- AddCommGroupstatement and proof · cited by 12,871
- LinearOrderstatement and proof · cited by 8,572
- AddSubgroupstatement · cited by 3,232
- Factstatement and proof · cited by 2,726
- HasQuotient.Quotientstatement · cited by 2,301
- IsOrderedAddMonoidstatement and proof · cited by 1,659
- OrderTopologystatement and proof · cited by 1,355
- OpenPartialHomeomorph.toFun'statement and proof · cited by 745
- Archimedeanstatement and proof · cited by 603
- AddSubgroup.zmultiplesstatement and proof · cited by 493
- DiscreteTopologystatement and proof · cited by 373
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.