Theorems · Theorem · general topology
isUniformEmbedding_inl
∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β], IsUniformEmbedding Sum.inl- Cited by
- 0 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpaceUniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- Set.imageproof · cited by 5,609
- Set.preimageproof · cited by 4,946
- Set.rangeproof · cited by 4,705
- UniformSpacestatement and proof · cited by 2,040
- SProd.sprodproof · cited by 1,750
- uniformityproof · cited by 765
- Set.image_congrproof · cited by 533
- IsUniformEmbeddingstatement · cited by 107
- Prod.mk.etaproof · cited by 84
- Filter.image_mem_mapproof · cited by 39
- Sum.inl_injectiveproof · cited by 39
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.