Theorems · Theorem · general topology
Homeomorph.surjective
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
Function.Surjective ⇑h- Defined in
- Mathlib.Topology.Homeomorph.Defs
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses 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.
- DFunLike.coestatement · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- Homeomorphstatement and proof · cited by 725
- Equiv.surjectiveproof · cited by 198
- Homeomorph.toEquivproof · cited by 77
Cited by24
Results whose statement or proof uses this declaration.
- Homeomorph.isOpenQuotientMapproof · cited by 5
- AlgebraicGeometry.Scheme.Hom.opensRange_of_isIsoproof · cited by 4
- Complex.frontier_reProdImproof · cited by 3
- Complex.closure_reProdImproof · cited by 2
- TopologicalSpace.noetherianSpace_iff_of_homeomorphproof · cited by 2
- AlgebraicGeometry.isPullback_inl_inl_coprodMapproof · cited by 2
- Homeomorph.irreducibleSpace_iffproof · cited by 1
- AlgebraicGeometry.Proj.awayι_preimage_basicOpenproof · cited by 1
- isEmbedding_of_iSup_eq_top_of_preimage_subset_rangeproof · cited by 1
- IsHomeomorphicTrivialFiberBundle.surjective_projproof · cited by 1
- Homeomorph.isDenseEmbeddingproof · cited by 1
- Real.fromBinary_surjectiveproof · cited by 1