Theorems · Theorem · general topology
Topology.IsClosedEmbedding.isClosed_range
∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
Topology.IsClosedEmbedding f → IsClosed (Set.range f)The range of a closed embedding is a closed set.
- Defined in
- Mathlib.Topology.Defs.Induced
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Set.rangestatement · cited by 4,705
- IsClosedstatement · cited by 1,639
- Topology.IsClosedEmbeddingstatement and proof · cited by 195
Cited by41
Results whose statement or proof uses this declaration.
- Topology.IsClosedEmbedding.isClosedMapproof · cited by 19
- Topology.IsClosedEmbedding.measurableEmbeddingproof · cited by 16
- Topology.IsClosedEmbedding.isCompact_preimageproof · cited by 12
- ModelWithCorners.isClosed_rangeproof · cited by 7
- Topology.IsClosedEmbedding.map_tsumproof · cited by 6
- Topology.IsClosedEmbedding.locallyCompactSpaceproof · cited by 3
- Topology.IsClosedEmbedding.of_compproof · cited by 3
- AlgebraicGeometry.ext_of_isDominant_of_isSeparatedproof · cited by 3
- AlgebraicGeometry.isClosed_singleton_iff_isClosedImmersionproof · cited by 2
- Topology.IsClosedEmbedding.map_tprodproof · cited by 2
- ContinuousMap.exists_extensionproof · cited by 2
- Topology.IsClosedEmbedding.polishSpaceproof · cited by 2