Theorems · Theorem · general topology
Topology.IsOpenEmbedding.inr
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Topology.IsOpenEmbedding Sum.inr- Defined in
- Mathlib.Topology.Constructions.SumProd
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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.IsOpenEmbeddingstatement · cited by 231
- Sum.inr_injectiveproof · cited by 40
- Topology.IsOpenEmbedding.of_continuous_injective_isOpenMapproof · cited by 13
- continuous_inrproof · cited by 9
- isOpenMap_inrproof · cited by 3
Cited by12
Results whose statement or proof uses this declaration.
- ChartedSpace.sum_chartAt_inrstatement and proof · cited by 7
- sum_chartAt_inr_applyproof · cited by 6
- Topology.IsEmbedding.inrproof · cited by 5
- ContMDiff.sumElimproof · cited by 4
- ContMDiff.inrproof · cited by 3
- nhds_inrproof · cited by 2
- isOpen_range_inrproof · cited by 2
- TopCat.binaryCofan_isColimit_iffproof · cited by 1
- ChartedSpace.sumOfNonemptyproof · cited by 1
- TopologicalSpace.separableSpace_sum_iffproof · cited by 0
- TopologicalSpace.IsTopologicalBasis.sumproof · cited by 0
- ChartedSpace.mem_atlas_sumstatement and proof · cited by 0