Theorems · Theorem · general topology
Topology.IsOpenEmbedding.continuous
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
Topology.IsOpenEmbedding f → Continuous f- Defined in
- Mathlib.Topology.Maps.Basic
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Continuousstatement · cited by 2,592
- Topology.IsOpenEmbeddingstatement and proof · cited by 231
- Topology.IsEmbedding.continuousproof · cited by 51
- Topology.IsOpenEmbedding.isEmbeddingproof · cited by 22
Cited by24
Results whose statement or proof uses this declaration.
- Topology.IsConstructible.preimage_of_isOpenEmbeddingproof · cited by 6
- Topology.IsLocallyConstructible.preimage_of_isOpenEmbeddingproof · cited by 3
- Topology.IsOpenEmbedding.isQuasiSeparated_iffproof · cited by 3
- Topology.isOpenEmbedding_iff_continuous_injective_isOpenMapproof · cited by 2
- Topology.IsOpenEmbedding.quasiSoberproof · cited by 2
- Topology.IsOpenEmbedding.accPt_comap_iffproof · cited by 2
- Topology.IsOpenEmbedding.coborder_preimageproof · cited by 1
- Topology.IsOpenEmbedding.coheight_eqproof · cited by 1
- Topology.IsOpenEmbedding.coheight_mapstatement and proof · cited by 1
- Topology.IsOpenEmbedding.compacts_mapstatement · cited by 1
- TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbeddingproof · cited by 1
- contMDiff_isOpenEmbeddingproof · cited by 1