Theorems · Theorem · general topology
Topology.IsClosedEmbedding.isClosed_iff_image_isClosed
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Topology.IsClosedEmbedding f → ∀ {s : Set X}, IsClosed s ↔ IsClosed (f '' s)- Defined in
- Mathlib.Topology.Maps.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Set.imagestatement and proof · cited by 5,609
- IsClosedstatement and proof · cited by 1,639
- Topology.IsClosedEmbeddingstatement and proof · cited by 195
- IsClosed.preimageproof · cited by 138
- Topology.IsEmbedding.injectiveproof · cited by 103
- Set.preimage_image_eqproof · cited by 87
- Topology.IsClosedEmbedding.toIsEmbeddingproof · cited by 27
- Topology.IsClosedEmbedding.continuousproof · cited by 25
- Topology.IsClosedEmbedding.isClosedMapproof · cited by 19
Cited by13
Results whose statement or proof uses this declaration.
- Topology.IsClosedEmbedding.of_comp_iffproof · cited by 3
- loc_compact_Haus_tot_disc_of_zero_dimproof · cited by 2
- Profinite.exists_lift_of_finite_of_injective_of_surjectiveproof · cited by 1
- MeasureTheory.hasDerivAt_resolventTransformproof · cited by 1
- Topology.IsClosedEmbedding.preimage_closedPointsproof · cited by 1
- isClosed_preCantorSetproof · cited by 1
- MeasureTheory.norm_resolvent_le_inv_infDist_supportproof · cited by 1
- MeasureTheory.analyticOn_resolventTransformproof · cited by 0
- CStarAlgebra.isClosed_nonnegproof · cited by 0
- Topology.IsClosedEmbedding.isClosed_iff_preimage_isClosedproof · cited by 0
- AlgebraicGeometry.IsClosedImmersion.of_comp_isClosedImmersionproof · cited by 0
- ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotientproof · cited by 0