Theorems · Theorem · general topology
subset_closure_inter_of_isPreirreducible_of_isOpen
∀ {X : Type u_1} [inst : TopologicalSpace X] {S U : Set X},
IsPreirreducible S → IsOpen U → (S ∩ U).Nonempty → S ⊆ closure (S ∩ U)A nonempty open subset of a preirreducible subspace is dense in the subspace.
- Defined in
- Mathlib.Topology.Irreducible
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 66 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.
Cites10
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
- Compl.complproof · cited by 2,925
- Set.Nonemptystatement and proof · cited by 2,627
- IsOpenstatement and proof · cited by 2,400
- closurestatement and proof · cited by 1,254
- subset_closureproof · cited by 309
- IsClosed.isOpen_complproof · cited by 126
- IsPreirreduciblestatement and proof · cited by 43
- Set.inter_compl_nonempty_iffproof · cited by 6
Cited by6
Results whose statement or proof uses this declaration.
- closure_sUnion_irreducibleComponents_sdiff_singletonproof · cited by 2
- isPreirreducible_iff_subset_closure_inter_openproof · cited by 1
- AlgebraicGeometry.genericPoint_eq_of_isOpenImmersionproof · cited by 1
- preimage_mem_irreducibleComponents_of_isPreirreducible_fiberproof · cited by 1
- TopologicalSpace.IsOpenCover.quasiSober_iff_forallproof · cited by 1
- closure_image_preimage_of_isPreirreducibleproof · cited by 0