Theorems · Theorem · general topology
Topology.IsOpenEmbedding.isOpen_range
∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
Topology.IsOpenEmbedding f → IsOpen (Set.range f)The range of an open embedding is an open set.
- Defined in
- Mathlib.Topology.Defs.Induced
- Cited by
- 33 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
- IsOpenstatement · cited by 2,400
- Topology.IsOpenEmbeddingstatement and proof · cited by 231
Cited by33
Results whose statement or proof uses this declaration.
- Topology.IsOpenEmbedding.isOpenMapproof · cited by 50
- Topology.IsOpenEmbedding.map_nhds_eqproof · cited by 22
- Topology.IsOpenEmbedding.measurableEmbeddingproof · cited by 5
- JacobsonSpace.of_isOpenEmbeddingproof · cited by 3
- Topology.IsOpenEmbedding.locallyCompactSpaceproof · cited by 3
- Set.restrictPreimage_isOpenEmbeddingproof · cited by 2
- isOpen_range_inlproof · cited by 2
- isOpen_range_inrproof · cited by 2
- TopCat.pullback_map_isOpenEmbeddingproof · cited by 2
- Topology.IsOpenEmbedding.locallyConnectedSpaceproof · cited by 2
- Topology.IsOpenEmbedding.locallyPathConnectedSpaceproof · cited by 2
- Topology.IsConstructible.image_of_isOpenEmbeddingproof · cited by 2