Theorems · Theorem · general topology
Topology.IsEmbedding.toIsInducing
∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
Topology.IsEmbedding f → Topology.IsInducing f- Defined in
- Mathlib.Topology.Defs.Induced
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- Topology.IsEmbeddingstatement and proof · cited by 294
- Topology.IsInducingstatement · cited by 266
Cited by49
Results whose statement or proof uses this declaration.
- Topology.IsEmbedding.isInducingproof · cited by 47
- Topology.IsEmbedding.closure_eq_preimage_closure_imageproof · cited by 7
- Topology.IsEmbedding.secondCountableTopologyproof · cited by 6
- IsUniformEmbedding.isDenseEmbeddingproof · cited by 4
- Topology.IsClosedEmbedding.of_compproof · cited by 3
- Topology.IsEmbedding.piMapproof · cited by 3
- Topology.IsEmbedding.toHomeomorphOfSurjectiveproof · cited by 3
- Topology.IsEmbedding.to_isometrystatement and proof · cited by 3
- TopologicalSpace.Compacts.isPreconnected_nonempty_finite_subsetsproof · cited by 2
- Topology.IsEmbedding.map_nhds_eqproof · cited by 2
- Topology.IsEmbedding.map_nhds_of_memproof · cited by 2
- AlgebraicGeometry.Scheme.Hom.isDiscrete_preimage_singletonproof · cited by 2