Theorems · Inductive type · general topology
R1Space
(X : Type u_3) → [TopologicalSpace X] → Prop
A topological space is called a preregular (a.k.a. R₁) space, if any two topologically distinguishable points have disjoint neighbourhoods.
- Defined in
- Mathlib.Topology.Separation.Basic
- Cited by
- 125 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
Cited by131
Results whose statement or proof uses this declaration.
- IsCompact.closurestatement and proof · cited by 25
- IsCompact.closure_of_subsetstatement and proof · cited by 15
- tendsto_nhds_unique_inseparablestatement and proof · cited by 10
- MeasureTheory.Content.measurestatement and proof · cited by 10
- IsCompact.measure_closurestatement and proof · cited by 10
- IsCompact.closure_subset_of_isOpenstatement and proof · cited by 9
- MeasureTheory.Content.innerContent_iUnion_natstatement and proof · cited by 6
- MeasureTheory.Content.measure_applystatement and proof · cited by 6
- MeasureTheory.Content.outerMeasure_opensstatement and proof · cited by 6
- SeparatedNhds.of_isCompact_isCompact_isClosedstatement and proof · cited by 6
- MeasurableSet.exists_isCompact_isClosed_sdiff_ltstatement and proof · cited by 5
- Filter.coclosedCompact_eq_cocompactstatement and proof · cited by 5