Regular

📁 Source: Mathlib/Topology/Separation/Regular.lean

Statistics

Metric	Count
Definitions `Regular`, `Regular`, `CompletelyNormalSpace`, `NormalSpace`, `RegularSpace`, `T25Space`, `T3Space`, `T4Space`, `T5Space`	9
Theorems `completely_normal`, `of_forall_isOpen_normalSpace`, `of_forall_normalSpace`, `of_regularSpace_secondCountableTopology`, `toNormalSpace`, `t2`, `nhds_closure`, `normalSpace`, `t25Space`, `t3Space`, `t4Space`, `t5Space`, `HasSeparatingCover`, `closure_eq_nhdsKer`, `exists_isOpen_closure_subset`, `lift'_closure_nhdsSet`, `nhdsSet_basis_isCompact_isClosed`, `normal`, `of_compactSpace_r1Space`, `of_regularSpace_lindelofSpace`, `of_regularSpace_secondCountableTopology`, `inf`, `of_exists_mem_nhds_isClosed_subset`, `of_hasBasis`, `of_lift'_closure`, `of_lift'_closure_le`, `regular`, `t3Space_iff_t0Space`, `of_isCompact_isClosed`, `instNormalSpace`, `instT25Space`, `t3Space`, `of_injective_continuous`, `t2Space`, `t2_5`, `t25Space`, `toRegularSpace`, `toT0Space`, `t3Space`, `toNormalSpace`, `toT1Space`, `of_forall_isOpen_t4Space`, `of_forall_t4Space`, `toCompletelyNormalSpace`, `toT1Space`, `toT4Space`, `exists_closure_subset`, `nhds_basis_closure`, `normalSpace`, `t4Space`, `completelyNormalSpace`, `t25Space`, `t3Space`, `t5Space`, `regularSpace`, `instCompletelyNormalSpace`, `instT3Space`, `instT4Space`, `instT5Space`, `closed_nhds_basis`, `completelyNormalSpace_iff_forall_isOpen_normalSpace`, `completelyNormalSpace_iff_forall_normalSpace`, `connectedComponent_eq_iInter_isClopen`, `disjoint_lift'_closure_nhds`, `disjoint_nested_nhds`, `disjoint_nested_nhds_of_not_inseparable`, `disjoint_nhdsSet_nhds`, `disjoint_nhdsSet_nhdsSet`, `disjoint_nhds_nhdsSet`, `exists_compact_closed_between`, `exists_mem_nhds_isClosed_subset`, `exists_nhds_disjoint_closure`, `exists_open_between_and_isCompact_closure`, `exists_open_nhds_disjoint_closure`, `hasBasis_nhds_closure`, `hasBasis_opens_closure`, `instCompletelyNormalSpaceSubtype`, `instR1Space`, `instRegularSpaceForall`, `instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space`, `instRegularSpaceProd`, `instRegularSpaceSubtype`, `instT3Space`, `instT3SpaceForall`, `instT3SpaceProd`, `instT3SpaceSeparationQuotientOfRegularSpace`, `instT4SpaceOfT1SpaceOfNormalSpace`, `instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space`, `instT5SpaceSubtype`, `lift'_nhds_closure`, `normal_exists_closure_subset`, `normal_separation`, `regularSpace_TFAE`, `regularSpace_generateFrom`, `regularSpace_iInf`, `regularSpace_iff`, `regularSpace_induced`, `regularSpace_sInf`, `t5Space_iff_forall_isOpen_t4Space`, `t5Space_iff_forall_t4Space`	100
Total	109

Affine.Simplex

Definitions

Name	Category	Theorems
`Regular` 📖	MathDef	1 math math: `regular_reindex_iff`

CategoryTheory

Definitions

Name	Category	Theorems
`Regular` 📖	CompData	—

CompletelyNormalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completely_normal` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure`	`Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet`	—	—
`of_forall_isOpen_normalSpace` 📖	mathematical	`NormalSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`CompletelyNormalSpace`	—	`completelyNormalSpace_iff_forall_isOpen_normalSpace`
`of_forall_normalSpace` 📖	mathematical	`NormalSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`CompletelyNormalSpace`	—	`completelyNormalSpace_iff_forall_normalSpace`
`of_regularSpace_secondCountableTopology` 📖	mathematical	—	`CompletelyNormalSpace`	—	`of_forall_normalSpace` `NormalSpace.of_regularSpace_secondCountableTopology` `instRegularSpaceSubtype` `TopologicalSpace.Subtype.secondCountableTopology`
`toNormalSpace` 📖	mathematical	—	`NormalSpace`	—	`separatedNhds_iff_disjoint` `completely_normal` `IsClosed.closure_eq`

ConnectedComponents

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2` 📖	mathematical	—	`T2Space` `ConnectedComponents` `instTopologicalSpace`	—	`Function.Surjective.forall₂` `surjective_coe` `connectedComponent_disjoint` `coe_ne_coe` `IsCompact.elim_finite_subfamily_closed` `IsClosed.isCompact` `isClosed_connectedComponent` `Set.disjoint_iff_inter_eq_empty` `connectedComponent_eq_iInter_isClopen` `isClopen_biInter_finset` `Set.subset_iInter₂` `IsClopen.connectedComponent_subset` `IsClopen.biUnion_connectedComponent_eq` `connectedComponents_preimage_image` `IsClopen.isOpen` `IsClopen.compl` `Topology.IsQuotientMap.isClopen_preimage` `isQuotientMap_coe` `Set.Nonempty.ne_empty` `mem_connectedComponent` `disjoint_compl_left`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds_closure` 📖	mathematical	`Filter.HasBasis` `nhds`	`closure`	—	`lift'_closure` `lift'_nhds_closure`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normalSpace` 📖	mathematical	—	`NormalSpace`	—	`Topology.IsClosedEmbedding.normalSpace` `isClosedEmbedding`
`t25Space` 📖	mathematical	—	`T25Space`	—	`Topology.IsEmbedding.t25Space` `isEmbedding`
`t3Space` 📖	mathematical	—	`T3Space`	—	`Topology.IsEmbedding.t3Space` `isEmbedding`
`t4Space` 📖	mathematical	—	`T4Space`	—	`Topology.IsClosedEmbedding.t4Space` `isClosedEmbedding`
`t5Space` 📖	mathematical	—	`T5Space`	—	`Topology.IsEmbedding.t5Space` `Topology.IsClosedEmbedding.toIsEmbedding` `isClosedEmbedding`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`HasSeparatingCover` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`HasSeparatingCover`	—	`isEmpty_or_nonempty` `Set.subset_eq_empty` `Set.univ_eq_empty_iff` `hasSeparatingCovers_iff_separatedNhds` `SeparatedNhds.empty_left` `List.TFAE.out` `regularSpace_TFAE` `compl_mem_nhds` `Set.disjoint_left` `isOpen_interior` `closure_subset_iff` `interior_subset` `mem_interior_iff_mem_nhds` `isOpen_empty` `SeparatedNhds.disjoint_closure_left` `IsLindelof.indexed_countable_subcover` `isLindelof` `Set.mem_iUnion`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq_nhdsKer` 📖	mathematical	`IsCompact`	`closure` `nhdsKer`	—	`subset_antisymm` `Set.instAntisymmSubset` `nhdsKer.eq_1` `lift'_closure_nhdsSet` `iInf_congr_Prop` `Filter.ker_iInf` `Set.iInter_congr_Prop` `Filter.ker_principal` `Filter.disjoint_iff` `disjoint_nhdsSet_nhds` `Set.disjoint_iff` `mem_of_mem_nhds`
`exists_isOpen_closure_subset` 📖	mathematical	`IsCompact` `Set` `Filter` `Filter.instMembership` `nhdsSet`	`IsOpen` `Set.instHasSubset` `closure`	—	`disjoint_nhdsSet_left` `closure_compl` `Filter.HasBasis.disjoint_iff` `hasBasis_nhdsSet` `Set.Subset.trans` `closure_minimal` `Disjoint.subset_compl_right` `IsOpen.isClosed_compl` `Set.compl_subset_comm`
`lift'_closure_nhdsSet` 📖	mathematical	`IsCompact`	`Filter.lift'` `nhdsSet` `closure`	—	`le_antisymm` `exists_isOpen_closure_subset` `Filter.mem_of_superset` `Filter.mem_lift'` `IsOpen.mem_nhdsSet` `Filter.le_lift'_closure`
`nhdsSet_basis_isCompact_isClosed` 📖	mathematical	`IsCompact`	`Filter.HasBasis` `Set` `nhdsSet` `Filter` `Filter.instMembership` `IsClosed`	—	`Filter.hasBasis_self` `Filter.HasBasis.forall_iff` `hasBasis_nhdsSet` `exists_compact_closed_between` `subset_interior_iff_mem_nhdsSet`

NormalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normal` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`SeparatedNhds`	—	—
`of_compactSpace_r1Space` 📖	mathematical	—	`NormalSpace`	—	`SeparatedNhds.of_isCompact_isCompact_isClosed` `IsClosed.isCompact`
`of_regularSpace_lindelofSpace` 📖	mathematical	—	`NormalSpace`	—	`hasSeparatingCovers_iff_separatedNhds` `IsClosed.HasSeparatingCover` `Disjoint.symm`
`of_regularSpace_secondCountableTopology` 📖	mathematical	—	`NormalSpace`	—	`of_regularSpace_lindelofSpace` `HereditarilyLindelof.to_Lindelof` `SecondCountableTopology.toHereditarilyLindelof`

RegularSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf` 📖	mathematical	—	`RegularSpace` `TopologicalSpace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`inf_eq_iInf` `regularSpace_iInf`
`of_exists_mem_nhds_isClosed_subset` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `IsClosed` `Set.instHasSubset`	`RegularSpace`	—	`List.TFAE.out` `regularSpace_TFAE`
`of_hasBasis` 📖	mathematical	`Filter.HasBasis` `nhds` `IsClosed`	`RegularSpace`	—	`of_lift'_closure` `Filter.HasBasis.lift'_closure_eq_self`
`of_lift'_closure` 📖	mathematical	`Filter.lift'` `nhds` `closure`	`RegularSpace`	—	`List.TFAE.out` `regularSpace_TFAE`
`of_lift'_closure_le` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.lift'` `nhds` `closure`	`RegularSpace`	—	`List.TFAE.out` `regularSpace_TFAE`
`regular` 📖	mathematical	`Set` `Set.instMembership`	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet` `nhds`	—	—
`t3Space_iff_t0Space` 📖	mathematical	—	`T3Space` `T0Space`	—	`T3Space.toT0Space` `instT3Space`

SeparatedNhds

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isCompact_isClosed` 📖	mathematical	`IsCompact` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`SeparatedNhds`	—	`IsCompact.disjoint_nhdsSet_left` `IsClosed.closure_eq`

SeparationQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNormalSpace` 📖	mathematical	—	`NormalSpace` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient`	—	`separatedNhds_iff_disjoint` `Filter.disjoint_comap_iff` `comap_mk_nhdsSet` `disjoint_nhdsSet_nhdsSet` `IsClosed.preimage` `Disjoint.preimage`

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instT25Space` 📖	mathematical	—	`T25Space` `instTopologicalSpaceSubtype`	—	`Topology.IsEmbedding.t25Space` `Topology.IsEmbedding.subtypeVal`
`t3Space` 📖	mathematical	—	`T3Space` `instTopologicalSpaceSubtype`	—	`Topology.IsEmbedding.t3Space` `Topology.IsEmbedding.subtypeVal`

T25Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_injective_continuous` 📖	mathematical	`Continuous`	`T25Space`	—	`Filter.Tendsto.disjoint` `tendsto_lift'_closure_nhds` `t2_5`
`t2Space` 📖	mathematical	—	`T2Space`	—	`t2Space_iff_disjoint_nhds` `Disjoint.mono` `Filter.le_lift'_closure` `disjoint_lift'_closure_nhds`
`t2_5` 📖	mathematical	—	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `Filter.lift'` `nhds` `closure`	—	—

T3Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t25Space` 📖	mathematical	—	`T25Space`	—	`lift'_nhds_closure` `toRegularSpace` `t0Space_iff_or_notMem_closure` `toT0Space` `nhdsSet_singleton` `Disjoint.symm`
`toRegularSpace` 📖	mathematical	—	`RegularSpace`	—	—
`toT0Space` 📖	mathematical	—	`T0Space`	—	—

T4Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t3Space` 📖	mathematical	—	`T3Space`	—	`T1Space.t0Space` `toT1Space` `nhdsSet_singleton` `SeparatedNhds.disjoint_nhdsSet` `normal_separation` `toNormalSpace` `isClosed_singleton` `Set.disjoint_singleton_right`
`toNormalSpace` 📖	mathematical	—	`NormalSpace`	—	—
`toT1Space` 📖	mathematical	—	`T1Space`	—	—

T5Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_forall_isOpen_t4Space` 📖	mathematical	`T4Space` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`T5Space`	—	`t5Space_iff_forall_isOpen_t4Space`
`of_forall_t4Space` 📖	mathematical	`T4Space` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`T5Space`	—	`t5Space_iff_forall_t4Space`
`toCompletelyNormalSpace` 📖	mathematical	—	`CompletelyNormalSpace`	—	—
`toT1Space` 📖	mathematical	—	`T1Space`	—	—
`toT4Space` 📖	mathematical	—	`T4Space`	—	`toT1Space` `CompletelyNormalSpace.toNormalSpace` `toCompletelyNormalSpace`

TopologicalSpace.IsTopologicalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_closure_subset` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis` `Set` `Filter` `Filter.instMembership` `nhds`	`Set.instMembership` `Set.instHasSubset` `closure`	—	`Filter.HasBasis.mem_iff` `Filter.HasBasis.nhds_closure` `nhds_hasBasis`
`nhds_basis_closure` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis`	`Filter.HasBasis` `Set` `nhds` `Set.instMembership` `closure`	—	`Filter.HasBasis.nhds_closure` `nhds_hasBasis`

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normalSpace` 📖	mathematical	`Topology.IsClosedEmbedding`	`NormalSpace`	—	`NormalSpace.normal` `isClosedMap` `Set.disjoint_image_of_injective` `Topology.IsEmbedding.injective` `toIsEmbedding` `SeparatedNhds.mono` `SeparatedNhds.preimage` `continuous` `Set.subset_preimage_image`
`t4Space` 📖	mathematical	`Topology.IsClosedEmbedding`	`T4Space`	—	`Topology.IsEmbedding.t1Space` `T4Space.toT1Space` `isEmbedding` `normalSpace` `T4Space.toNormalSpace`

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completelyNormalSpace` 📖	mathematical	`Topology.IsEmbedding`	`CompletelyNormalSpace`	—	`Topology.IsInducing.nhdsSet_eq_comap` `isInducing` `Filter.disjoint_comap` `CompletelyNormalSpace.completely_normal` `Set.subset_compl_iff_disjoint_left` `Set.image_subset_iff` `Set.preimage_compl` `closure_eq_preimage_closure_image` `Set.subset_compl_iff_disjoint_right`
`t25Space` 📖	mathematical	`Topology.IsEmbedding`	`T25Space`	—	`T25Space.of_injective_continuous` `injective` `continuous`
`t3Space` 📖	mathematical	`Topology.IsEmbedding`	`T3Space`	—	`t0Space` `T3Space.toT0Space` `Topology.IsInducing.regularSpace` `T3Space.toRegularSpace` `isInducing`
`t5Space` 📖	mathematical	`Topology.IsEmbedding`	`T5Space`	—	`t1Space` `T5Space.toT1Space` `completelyNormalSpace` `T5Space.toCompletelyNormalSpace` `CompletelyNormalSpace.completely_normal`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`regularSpace` 📖	mathematical	`Topology.IsInducing`	`RegularSpace`	—	`RegularSpace.of_hasBasis` `nhds_eq_comap` `Filter.HasBasis.comap` `closed_nhds_basis` `IsClosed.preimage` `continuous`

ULift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompletelyNormalSpace` 📖	mathematical	—	`CompletelyNormalSpace` `topologicalSpace`	—	`Topology.IsEmbedding.completelyNormalSpace` `Topology.IsEmbedding.uliftDown`
`instT3Space` 📖	mathematical	—	`T3Space` `topologicalSpace`	—	`Topology.IsEmbedding.t3Space` `Topology.IsEmbedding.uliftDown`
`instT4Space` 📖	mathematical	—	`T4Space` `topologicalSpace`	—	`Topology.IsClosedEmbedding.t4Space` `Topology.IsClosedEmbedding.uliftDown`
`instT5Space` 📖	mathematical	—	`T5Space` `topologicalSpace`	—	`Topology.IsEmbedding.t5Space` `Topology.IsEmbedding.uliftDown`

(root)

Definitions

Name	Category	Theorems
`CompletelyNormalSpace` 📖	CompData	18 math math: `CompletelyNormalSpace.of_regularSpace_secondCountableTopology`, `T5Space.toCompletelyNormalSpace`, `completelyNormalSpace_iff_forall_normalSpace`, `instCompletelyNormalSpaceSubtype`, `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity`, `PerfectlyNormalSpace.toCompletelyNormalSpace`, `DomAddAct.instCompletelyNormalSpace`, `instCompletelyNormalSpaceOfIsUpperSet`, `OrderTopology.completelyNormalSpace`, `instCompletelyNormalSpaceProp`, `ULift.instCompletelyNormalSpace`, `CompletelyNormalSpace.of_forall_isOpen_normalSpace`, `instCompletelyNormalSpaceOfIsLowerSet`, `DomMulAct.instCompletelyNormalSpace`, `UniformSpace.completelyNormalSpace_of_hasAntitoneBasis`, `completelyNormalSpace_iff_forall_isOpen_normalSpace`, `Topology.IsEmbedding.completelyNormalSpace`, `CompletelyNormalSpace.of_forall_normalSpace`
`NormalSpace` 📖	CompData	16 math math: `SeparationQuotient.instNormalSpace`, `NormalSpace.of_regularSpace_secondCountableTopology`, `PerfectlyNormalSpace.toNormalSpace`, `completelyNormalSpace_iff_forall_normalSpace`, `DomMulAct.instNormalSpace`, `OnePoint.instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space`, `T4Space.toNormalSpace`, `CompletelyNormalSpace.toNormalSpace`, `Topology.IsClosedEmbedding.normalSpace`, `Homeomorph.normalSpace`, `NormalSpace.of_regularSpace_lindelofSpace`, `IsClosed.not_normal_of_continuum_le_mk`, `completelyNormalSpace_iff_forall_isOpen_normalSpace`, `NormalSpace.of_compactSpace_r1Space`, `instNormalSpaceOfPseudoMetrizableSpace`, `DomAddAct.instNormalSpace`
`RegularSpace` 📖	CompData	23 math math: `DomMulAct.instRegularSpace`, `instRegularSpaceSubtype`, `IsTopologicalAddGroup.regularSpace`, `RegularSpace.of_exists_mem_nhds_isClosed_subset`, `RegularSpace.of_hasBasis`, `TopologicalSpace.PseudoMetrizableSpace.regularSpace`, `RegularSpace.inf`, `UniformSpace.to_regularSpace`, `regularSpace_induced`, `regularSpace_generateFrom`, `DomAddAct.instRegularSpace`, `ContinuousMap.instRegularSpace`, `regularSpace_iff`, `regularSpace_TFAE`, `RegularSpace.of_lift'_closure_le`, `ContinuousMapZero.instRegularSpace`, `RegularSpace.of_lift'_closure`, `Topology.IsInducing.regularSpace`, `instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space`, `CompletelyRegularSpace.instRegularSpace`, `instRegularSpaceProd`, `T3Space.toRegularSpace`, `IsTopologicalGroup.regularSpace`
`T25Space` 📖	CompData	7 math math: `Topology.IsEmbedding.t25Space`, `DomMulAct.instT25Space`, `Subtype.instT25Space`, `T3Space.t25Space`, `T25Space.of_injective_continuous`, `DomAddAct.instT25Space`, `Homeomorph.t25Space`
`T3Space` 📖	CompData	24 math math: `QuotientAddGroup.instT3Space`, `DomAddAct.instT3Space`, `DomMulAct.instT3Space`, `Submodule.t3_quotient_of_isClosed`, `ContDiffMapSupportedIn.instT3Space`, `instT3SpaceSeparationQuotientOfRegularSpace`, `RegularSpace.t3Space_iff_t0Space`, `instT3Space`, `ULift.instT3Space`, `Topology.IsEmbedding.t3Space`, `Subtype.t3Space`, `QuotientGroup.instT3Space`, `ContinuousMap.instT3Space`, `T35Space.instT3space`, `ContinuousAlternatingMap.instT3Space`, `ContinuousMultilinearMap.instT3Space`, `ContinuousLinearMapWOT.instT3Space`, `UpperHalfPlane.instT3Space`, `CStarMatrix.instT3Space`, `T4Space.t3Space`, `Homeomorph.t3Space`, `instT3SpaceProd`, `ContinuousMapZero.instT3Space`, `TestFunction.instT3Space`
`T4Space` 📖	CompData	17 math math: `instT4SpaceOfT1SpaceOfNormalSpace`, `ENNReal.instT4Space`, `DomAddAct.instT4Space`, `Metric.t4Space`, `UpperHalfPlane.instT4Space`, `Topology.IsClosedEmbedding.t4Space`, `exists_opensMeasurableSpace_of_countablySeparated`, `t5Space_iff_forall_t4Space`, `T4Space.of_paracompactSpace_t2Space`, `Homeomorph.t4Space`, `t5Space_iff_forall_isOpen_t4Space`, `EMetric.t4Space`, `T5Space.toT4Space`, `instT4SpaceOfMetrizableSpace`, `DomMulAct.instT4Space`, `exists_borelSpace_of_countablyGenerated_of_separatesPoints`, `ULift.instT4Space`
`T5Space` 📖	CompData	16 math math: `T6Space.toT5Space`, `Topology.IsEmbedding.t5Space`, `EReal.instT5Space`, `DomMulAct.instT5Space`, `ENNReal.instT5Space`, `OrderTopology.t5Space`, `Homeomorph.t5Space`, `T5Space.of_forall_t4Space`, `WithZeroTopology.t5Space`, `t5Space_iff_forall_t4Space`, `DomAddAct.instT5Space`, `instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space`, `T5Space.of_forall_isOpen_t4Space`, `instT5SpaceSubtype`, `t5Space_iff_forall_isOpen_t4Space`, `ULift.instT5Space`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closed_nhds_basis` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `Filter` `Filter.instMembership` `IsClosed`	—	`Filter.hasBasis_self` `exists_mem_nhds_isClosed_subset`
`completelyNormalSpace_iff_forall_isOpen_normalSpace` 📖	mathematical	—	`CompletelyNormalSpace` `NormalSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`CompletelyNormalSpace.toNormalSpace` `instCompletelyNormalSpaceSubtype` `IsClosed.isOpen_compl` `IsClosed.inter` `isClosed_closure` `Set.disjoint_left` `normal_separation` `IsClosed.preimage` `continuous_subtype_val` `Topology.IsInducing.isOpen_iff` `Topology.IsInducing.subtypeVal` `separatedNhds_iff_disjoint` `IsOpen.inter` `Set.inter_comm` `Subtype.preimage_val_subset_preimage_val_iff` `subset_closure` `Disjoint.notMem_of_mem_left`
`completelyNormalSpace_iff_forall_normalSpace` 📖	mathematical	—	`CompletelyNormalSpace` `NormalSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`CompletelyNormalSpace.toNormalSpace` `instCompletelyNormalSpaceSubtype` `completelyNormalSpace_iff_forall_isOpen_normalSpace`
`connectedComponent_eq_iInter_isClopen` 📖	mathematical	—	`connectedComponent` `Set.iInter` `Set` `IsClopen` `Set.instMembership`	—	`Set.Subset.antisymm` `connectedComponent_subset_iInter_isClopen` `IsPreconnected.subset_connectedComponent` `isClosed_iInter` `isPreconnected_iff_subset_of_fully_disjoint_closed` `normal_separation` `NormalSpace.of_regularSpace_lindelofSpace` `instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space` `instWeaklyLocallyCompactSpaceOfCompactSpace` `T2Space.r1Space` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `IsCompact.inter_iInter_nonempty` `IsClosed.isCompact` `IsOpen.isClosed_compl` `IsOpen.union` `Set.not_disjoint_iff_nonempty_inter` `Set.disjoint_compl_left_iff_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.union_subset_union` `isClopen_biInter_finset` `Set.mem_iInter₂` `Set.disjoint_iff_inter_eq_empty` `Set.not_nonempty_iff_eq_empty` `isClopen_inter_of_disjoint_cover_clopen` `Set.union_comm` `Disjoint.symm` `Set.Subset.trans` `Set.iInter_subset` `Set.mem_inter` `Set.inter_subset_right` `Disjoint.left_le_of_le_sup_right` `Disjoint.mono` `Set.mem_iInter` `Disjoint.left_le_of_le_sup_left`
`disjoint_lift'_closure_nhds` 📖	mathematical	—	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `Filter.lift'` `nhds` `closure`	—	`Filter.NeBot.ne` `nhds_neBot` `T25Space.t2_5`
`disjoint_nested_nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `IsClosed` `IsOpen` `Set.instHasSubset` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`disjoint_nested_nhds_of_not_inseparable` `T3Space.toRegularSpace` `Inseparable.eq` `T3Space.toT0Space`
`disjoint_nested_nhds_of_not_inseparable` 📖	mathematical	`Inseparable`	`Set` `Filter` `Filter.instMembership` `nhds` `IsClosed` `IsOpen` `Set.instHasSubset` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`r1_separation` `instR1Space` `exists_mem_nhds_isClosed_subset` `IsOpen.mem_nhds` `Filter.mem_of_superset`
`disjoint_nhdsSet_nhds` 📖	mathematical	—	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet` `nhds` `Set` `Set.instMembership` `closure`	—	`List.TFAE.out` `regularSpace_TFAE`
`disjoint_nhdsSet_nhdsSet` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet`	—	`SeparatedNhds.disjoint_nhdsSet` `normal_separation`
`disjoint_nhds_nhdsSet` 📖	mathematical	—	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhds` `nhdsSet` `Set` `Set.instMembership` `closure`	—	`disjoint_comm` `disjoint_nhdsSet_nhds`
`exists_compact_closed_between` 📖	mathematical	`IsCompact` `IsOpen` `Set` `Set.instHasSubset`	`IsClosed` `interior`	—	`exists_compact_between` `IsCompact.closure` `instR1Space` `isClosed_closure` `HasSubset.Subset.trans` `Set.instIsTransSubset` `interior_mono` `subset_closure` `IsCompact.closure_subset_of_isOpen`
`exists_mem_nhds_isClosed_subset` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`IsClosed` `Set.instHasSubset`	—	`List.TFAE.out` `regularSpace_TFAE`
`exists_nhds_disjoint_closure` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure`	—	`Filter.HasBasis.disjoint_iff` `Filter.HasBasis.lift'_closure` `Filter.basis_sets` `disjoint_lift'_closure_nhds`
`exists_open_between_and_isCompact_closure` 📖	mathematical	`IsCompact` `IsOpen` `Set` `Set.instHasSubset`	`closure`	—	`exists_compact_closed_between` `HasSubset.Subset.trans` `Set.instIsTransSubset` `closure_mono` `interior_subset` `le_of_eq` `IsClosed.closure_eq` `isOpen_interior` `IsCompact.closure_of_subset` `instR1Space`
`exists_open_nhds_disjoint_closure` 📖	mathematical	—	`Set` `Set.instMembership` `IsOpen` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure`	—	`Filter.HasBasis.disjoint_iff` `Filter.HasBasis.lift'_closure` `nhds_basis_opens` `disjoint_lift'_closure_nhds`
`hasBasis_nhds_closure` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `Filter` `Filter.instMembership` `closure`	—	`Filter.HasBasis.nhds_closure` `Filter.basis_sets`
`hasBasis_opens_closure` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `Set.instMembership` `IsOpen` `closure`	—	`Filter.HasBasis.nhds_closure` `nhds_basis_opens`
`instCompletelyNormalSpaceSubtype` 📖	mathematical	—	`CompletelyNormalSpace` `instTopologicalSpaceSubtype`	—	`Topology.IsEmbedding.completelyNormalSpace` `Topology.IsEmbedding.subtypeVal`
`instR1Space` 📖	mathematical	—	`R1Space`	—	`nhdsSet_singleton` `disjoint_nhdsSet_nhds` `specializes_iff_mem_closure`
`instRegularSpaceForall` 📖	mathematical	`RegularSpace`	`Pi.topologicalSpace`	—	`regularSpace_iInf` `regularSpace_induced`
`instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space` 📖	mathematical	—	`RegularSpace`	—	`RegularSpace.of_hasBasis` `isCompact_isClosed_basis_nhds`
`instRegularSpaceProd` 📖	mathematical	—	`RegularSpace` `instTopologicalSpaceProd`	—	`RegularSpace.inf` `regularSpace_induced`
`instRegularSpaceSubtype` 📖	mathematical	—	`RegularSpace` `instTopologicalSpaceSubtype`	—	`Topology.IsInducing.regularSpace` `Topology.IsEmbedding.isInducing` `Topology.IsEmbedding.subtypeVal`
`instT3Space` 📖	mathematical	—	`T3Space`	—	—
`instT3SpaceForall` 📖	mathematical	`T3Space`	`Pi.topologicalSpace`	—	`Pi.instT0Space` `T3Space.toT0Space` `instRegularSpaceForall` `T3Space.toRegularSpace`
`instT3SpaceProd` 📖	mathematical	—	`T3Space` `instTopologicalSpaceProd`	—	`Prod.instT0Space` `T3Space.toT0Space` `instRegularSpaceProd` `T3Space.toRegularSpace`
`instT3SpaceSeparationQuotientOfRegularSpace` 📖	mathematical	—	`T3Space` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient`	—	`SeparationQuotient.instT0Space` `Filter.disjoint_comap_iff` `SeparationQuotient.comap_mk_nhdsSet` `RegularSpace.regular` `IsClosed.preimage`
`instT4SpaceOfT1SpaceOfNormalSpace` 📖	mathematical	—	`T4Space`	—	—
`instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space` 📖	mathematical	—	`T5Space` `SeparationQuotient` `instTopologicalSpaceSeparationQuotient`	—	`List.TFAE.out` `t1Space_TFAE` `SeparationQuotient.t1Space_iff` `Filter.disjoint_comap_iff` `SeparationQuotient.comap_mk_nhdsSet` `CompletelyNormalSpace.completely_normal` `SeparationQuotient.preimage_mk_closure` `Disjoint.preimage`
`instT5SpaceSubtype` 📖	mathematical	—	`T5Space` `instTopologicalSpaceSubtype`	—	`Topology.IsEmbedding.t5Space` `Topology.IsEmbedding.subtypeVal`
`lift'_nhds_closure` 📖	mathematical	—	`Filter.lift'` `nhds` `closure`	—	`Filter.HasBasis.lift'_closure_eq_self` `closed_nhds_basis`
`normal_exists_closure_subset` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset`	`closure`	—	`Set.disjoint_left` `normal_separation` `isClosed_compl_iff` `Set.Subset.trans` `closure_minimal` `Disjoint.le_bot` `Set.compl_subset_comm`
`normal_separation` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`SeparatedNhds`	—	`NormalSpace.normal`
`regularSpace_TFAE` 📖	mathematical	—	`List.TFAE` `RegularSpace`	—	`regularSpace_iff` `Function.Surjective.forall` `compl_surjective` `forall_swap` `Filter.HasBasis.disjoint_iff_right` `nhds_basis_opens` `interior_compl` `Filter.HasBasis.le_basis_iff` `Filter.HasBasis.lift'_closure` `LE.le.antisymm` `Filter.le_lift'_closure` `Filter.HasBasis.mem_iff` `Filter.basis_sets` `Filter.mem_of_superset` `subset_closure` `isClosed_closure` `mem_interior_iff_mem_nhds` `Filter.disjoint_of_disjoint_of_mem` `disjoint_compl_left` `subset_interior_iff_mem_nhdsSet` `IsOpen.interior_eq` `IsClosed.isOpen_compl` `Set.subset_compl_comm` `mem_closure_iff_nhds_ne_bot` `Disjoint.eq_bot` `Disjoint.mono_right` `principal_le_nhdsSet` `Disjoint.symm` `IsClosed.closure_eq` `List.tfae_of_cycle`
`regularSpace_generateFrom` 📖	mathematical	`TopologicalSpace.generateFrom`	`RegularSpace` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet` `Compl.compl` `Set` `Set.instCompl` `nhds`	—	`RegularSpace.regular` `IsOpen.isClosed_compl` `TopologicalSpace.isOpen_generateFrom_of_mem` `Set.notMem_compl_iff` `Function.Involutive.surjective` `compl_involutive` `Set.compl_univ` `nhdsSet_empty` `Set.compl_sUnion` `Set.sInter_image` `Disjoint.mono` `nhdsSet_mono` `Set.iInter₂_subset` `le_refl` `isClosed_compl_iff`
`regularSpace_iInf` 📖	mathematical	`RegularSpace`	`iInf` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`regularSpace_sInf` `Set.forall_mem_range`
`regularSpace_iff` 📖	mathematical	—	`RegularSpace` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet` `nhds`	—	—
`regularSpace_induced` 📖	mathematical	—	`RegularSpace` `TopologicalSpace.induced`	—	`Topology.IsInducing.regularSpace` `Topology.IsInducing.induced`
`regularSpace_sInf` 📖	mathematical	`RegularSpace`	`InfSet.sInf` `TopologicalSpace` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`nhds_sInf` `iInf_subtype''` `Filter.HasBasis.iInf` `closed_nhds_basis` `RegularSpace.of_hasBasis` `isClosed_iInter` `IsClosed.mono` `sInf_le`
`t5Space_iff_forall_isOpen_t4Space` 📖	mathematical	—	`T5Space` `T4Space` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`T5Space.toT4Space` `instT5SpaceSubtype` `isOpen_univ` `t1Space_of_injective_of_continuous` `Set.mem_univ` `continuous_id` `T4Space.toT1Space` `completelyNormalSpace_iff_forall_isOpen_normalSpace` `T4Space.toNormalSpace`
`t5Space_iff_forall_t4Space` 📖	mathematical	—	`T5Space` `T4Space` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`T5Space.toT4Space` `instT5SpaceSubtype` `t5Space_iff_forall_isOpen_t4Space`

---

← Back to Index