Theorems · Theorem · general topology
TopologicalSpace.Opens.ext
∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α}, ↑U = ↑V → U = V- Defined in
- Mathlib.Topology.Sets.Opens
- Cited by
- 83 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
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.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- SetLike.coestatement and proof · cited by 8,199
- TopologicalSpace.Opensstatement and proof · cited by 2,040
- SetLike.coe_injectiveproof · cited by 374
Cited by83
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.preimage_image_eqproof · cited by 37
- AlgebraicGeometry.Scheme.Opens.opensRange_ιproof · cited by 29
- AlgebraicGeometry.isAffineOpen_topproof · cited by 26
- AlgebraicGeometry.IsAffineOpen.basicOpenproof · cited by 19
- AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRangeproof · cited by 17
- AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_infproof · cited by 15
- AlgebraicGeometry.iSup_affineOpens_eq_topproof · cited by 13
- AlgebraicGeometry.Scheme.OpenCover.iSup_opensRangeproof · cited by 9
- PrimeSpectrum.basicOpen_oneproof · cited by 7
- AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_topproof · cited by 5
- AlgebraicGeometry.basicOpen_eq_of_affineproof · cited by 5
- TopologicalSpace.Opens.iSup_defproof · cited by 5