Structures · Topology
QuasiSeparatedSpace
A topological space is quasi-separated if the intersections of any pairs of compact open subsets are still compact.
- Defined in
- Mathlib.Topology.QuasiSeparated
- Shape
- One type argument · adds inter_isCompact
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Every QuasiSeparatedSpace is also a
Provided automatically by
Concrete types that are instances2
- TopCat.carrier
- PrimeSpectrum
How is a type an instance?
Loading the hierarchy index…
Assumed by46
- isQuasiSeparated_univ
- IsCompact.isRetrocompact
- IsCompact.inter_of_isOpen
- AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated
- IsQuasiSeparated.of_quasiSeparatedSpace
- AlgebraicGeometry.quasiCompact_iff_compactSpace
- AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine_of_finite
- Topology.IsLocallyConstructible.isConstructible_of_subset_of_isCompact
- IsCompact.isConstructible
- Topology.IsLocallyConstructible.isConstructible
- AlgebraicGeometry.exists_appTop_π_eq_of_isLimit
- AlgebraicGeometry.Scheme.exists_isQuasiAffine_of_isLimit
- QuasiSeparatedSpace.isCompact_sInter
- Topology.IsConstructible.induction_of_isTopologicalBasis
- AlgebraicGeometry.Scheme.exists_isAffine_of_isLimit
- QuasiSeparatedSpace.isCompact_sInter_of_nonempty
- QuasiSeparatedSpace.isRetrocompact_iff_isCompact
- Topology.IsLocallyConstructible.inter_of_isOpen_isCompact
- AlgebraicGeometry.exists_isAffineOpen_preimage_eq
- QuasiSeparatedSpace.inter_isCompact
- AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine
- AlgebraicGeometry.exists_of_res_zero_of_qcqs_of_top
- QuasiSeparatedSpace.of_isOpenEmbedding
- Topology.IsOpenEmbedding.quasiSeparatedSpace
- AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat
- AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace
- AlgebraicGeometry.quasiCompact_of_compactSpace
- AlgebraicGeometry.instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj
- AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen
- TopologicalSpace.CompactOpens.instSemilatticeInf
- TopologicalSpace.CompactOpens.coe_inf
- isCompact_sInter_of_subset_constructibleTopologySubbasis
- TopologicalSpace.CompactOpens.instInf
- AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat
- AlgebraicGeometry.Scheme.Hom.isConstructible_image
- AlgebraicGeometry.nonempty_isColimit_Γ_mapCocone
- AlgebraicGeometry.Scheme.exists_π_app_comp_eq_of_locallyOfFinitePresentation
- AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace
- AlgebraicGeometry.pointsPi_injective
- AlgebraicGeometry.Scheme.preservesColimit_yoneda
- Topology.IsLocallyConstructible.iff_isConstructible_of_isOpenCover
- AlgebraicGeometry.QuasiSeparated.of_quasiSeparatedSpace
- AlgebraicGeometry.exists_of_res_eq_of_qcqs_of_top
- AlgebraicGeometry.Scheme.OpenCover.exists_of_isCofiltered_of_finite
- AlgebraicGeometry.instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat
- compactSpace_withConstructibleTopology