Theorems · Theorem · algebraic geometry
Topology.IsConstructible.isLocallyConstructible
∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, Topology.IsConstructible s → Topology.IsLocallyConstructible s- Defined in
- Mathlib.Topology.Constructible
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- Set.ofPredproof · cited by 6,101
- Set.univproof · cited by 3,945
- Subtype.range_coe_subtypeproof · cited by 170
- isOpen_univproof · cited by 112
- Topology.IsConstructiblestatement and proof · cited by 45
- IsRetrocompactproof · cited by 43
- IsOpen.isOpenEmbedding_subtypeValproof · cited by 32
- Topology.IsLocallyConstructiblestatement · cited by 22
- Topology.isConstructible_preimage_iff_of_isOpenEmbeddingproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- Topology.IsLocallyConstructible.emptyproof · cited by 3
- Topology.IsLocallyConstructible.univproof · cited by 2
- AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_imageproof · cited by 1
- Topology.IsLocallyConstructible.inter_of_isOpen_isCompactproof · cited by 1
- Topology.IsLocallyConstructible.iff_isConstructible_of_isOpenCoverproof · cited by 0
- IsRetrocompact.isLocallyConstructibleproof · cited by 0
- AlgebraicGeometry.Scheme.Hom.isConstructible_imageproof · cited by 0