Theorems · Theorem · Lie groups
DomMulAct.isEmbedding_mk_symm
∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsEmbedding ⇑DomMulAct.mk.symm- Cited by
- 0 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- Equivstatement · cited by 8,337
- Equiv.symmstatement · cited by 3,681
- Homeomorph.symmproof · cited by 365
- Topology.IsEmbeddingstatement · cited by 294
- Homeomorph.isEmbeddingproof · cited by 73
- DomMulActstatement · cited by 71
- DomMulAct.mkstatement · cited by 56
- DomMulAct.mkHomeomorphproof · cited by 17
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.