Theorems · Theorem · general topology
Topology.IsClosedEmbedding.isClosedMap
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Topology.IsClosedEmbedding f → IsClosedMap f- Defined in
- Mathlib.Topology.Maps.Basic
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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.IsClosedEmbeddingstatement and proof · cited by 195
- IsClosedMapstatement · cited by 138
- Topology.IsEmbedding.isInducingproof · cited by 47
- Topology.IsClosedEmbedding.isClosed_rangeproof · cited by 41
- Topology.IsClosedEmbedding.isEmbeddingproof · cited by 25
- Topology.IsInducing.isClosedMapproof · cited by 2
Cited by19
Results whose statement or proof uses this declaration.
- Topology.IsClosedEmbedding.compproof · cited by 14
- Topology.IsClosedEmbedding.isClosed_iff_image_isClosedproof · cited by 13
- IsClosed.isClosedMap_subtype_valproof · cited by 8
- Topology.IsClosedEmbedding.isProperMapproof · cited by 6
- Topology.IsClosedEmbedding.closure_image_eqproof · cited by 3
- Irrational.eventually_forall_le_dist_cast_divproof · cited by 2
- Topology.IsClosedEmbedding.normalSpaceproof · cited by 2
- range_cfcHomproof · cited by 1
- range_cfcₙHomproof · cited by 1
- BoundedContinuousFunction.tietze_extension_stepproof · cited by 1
- MeasureTheory.measurableEquiv_range_coe_nat_of_infinite_of_countableproof · cited by 1