Structures · Topology
R1Space
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
- Shape
- One type argument · adds specializes_or_disjoint_nhds
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances8
- DomMulAct
- DomAddAct
- ContinuousMapZero
- MeasureTheory.FiniteMeasure
- MeasureTheory.ProbabilityMeasure
- Subtype
- Prod
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by149
- IsCompact.closure
- IsCompact.closure_of_subset
- IsCompact.measure_closure
- MeasureTheory.Content.measure
- tendsto_nhds_unique_inseparable
- IsCompact.closure_subset_of_isOpen
- MeasureTheory.Content.outerMeasure_opens
- MeasureTheory.Content.measure_apply
- SeparatedNhds.of_isCompact_isCompact_isClosed
- MeasureTheory.Content.innerContent_iUnion_nat
- Filter.coclosedCompact_eq_cocompact
- MeasurableSet.exists_isCompact_isClosed_sdiff_lt
- HasCompactSupport.of_support_subset_isCompact
- R1Space.specializes_or_disjoint_nhds
- HasCompactSupport.intro
- aeconst_of_dense_setOfPred_preimage_vadd_ae
- aeconst_of_dense_setOfPred_preimage_smul_ae
- IsCompact.closure_subset_measurableSet
- IsCompact.closure_eq_biUnion_inseparable
- exists_compact_iff_hasCompactSupport
- MeasureTheory.isClosed_setOfPred_preimage_ae_eq
- MeasureTheory.Content.measure_eq_content_of_regular
- IsCompact.exists_isOpen_lt_of_lt
- MeasureTheory.Content.innerContent_iSup_nat
- IsCompact.exists_isOpen_lt_add
- MeasureTheory.MemLp.exists_hasCompactSupport_eLpNorm_sub_le
- aeconst_of_dense_setOfPred_preimage_smul_eq
- aeconst_of_dense_setOfPred_preimage_vadd_eq
- exists_continuousMap_one_of_isCompact_subset_isOpen
- MeasureTheory.Content.outerMeasure_preimage
- MeasureTheory.Content.outerMeasure_eq_iInf
- disjoint_nhds_nhds_iff_not_inseparable
- exists_tsupport_one_of_isOpen_isClosed
- MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure
- MeasureTheory.innerRegularWRT_isCompact_closure_iff
- MeasureTheory.Content.le_outerMeasure_compacts
- MeasureTheory.Content.outerMeasure_lt_top_of_isCompact
- IsDenseInducing.inseparable_extend
- MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero
- Filter.Tendsto.compMeasurePreservingLp
- exists_mem_nhds_isCompact_isClosed
- disjoint_nhds_nhds_iff_not_specializes
- exists_compact_iff_hasCompactMulSupport
- r1_separation
- CompactlySupportedContinuousMap.pullback_monoidHom_def
- uniformSpaceOfCompactR1
- MeasureTheory.Content.outerMeasure_interior_compacts
- MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt
- IsCompact.binary_compact_cover
- Inseparable.of_nhds_neBot
Ancestors0
No ancestors.