Theorems · Definition · general topology
StableUnderGeneralization
{X : Type u_1} → [TopologicalSpace X] → Set X → PropA subset S of a topological space is stable under specialization
if x ∈ S → y ∈ S for all y ⤳ x.
- Defined in
- Mathlib.Topology.Inseparable
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Specializesproof · cited by 176
Cited by24
Results whose statement or proof uses this declaration.
- IsOpen.stableUnderGeneralizationstatement · cited by 6
- StableUnderGeneralization.imagestatement · cited by 2
- GeneralizingMap.compproof · cited by 2
- GeneralizingMap.stableUnderGeneralization_imagestatement and proof · cited by 2
- PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRingstatement and proof · cited by 2
- Algebra.QuasiFiniteAt.isClopen_singletonproof · cited by 2
- stableUnderGeneralization_compl_iffstatement · cited by 2
- stableUnderSpecialization_compl_iffstatement · cited by 2
- StableUnderGeneralization.complstatement · cited by 1
- PrimeSpectrum.isOpen_of_stableUnderGeneralization_of_isConstructiblestatement and proof · cited by 1
- Topology.IsInducing.generalizingMapstatement and proof · cited by 1
- PrimeSpectrum.isQuotientMap_of_generalizingMapproof · cited by 1