CompletelyRegular

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

Statistics

Metric	Count
Definitions CompletelyRegularSpace, T35Space	2
Theorems completely_regular, completely_regular_isOpen, instRegularSpace, isTopologicalBasis_clopens_of_cardinalMk_lt_continuum, instCompletelyRegularSpace, instT3space, toCompletelyRegularSpace, toT0Space, instT35Space, t35Space, completelyRegularSpace, completelyRegularSpace_iInf, completelyRegularSpace_iff, completelyRegularSpace_iff_isInducing_stoneCechUnit, completelyRegularSpace_iff_isOpen, completelyRegularSpace_induced, completelyRegularSpace_inf, injective_stoneCechUnit_of_t35Space, instCompletelyRegularSpaceForall, instCompletelyRegularSpaceProd, instCompletelyRegularSpaceSubtype, instT35SpaceForall, instT35SpaceProd, instT35SpaceSubtype, isDenseEmbedding_stoneCechUnit, isDenseInducing_stoneCechUnit, isEmbedding_stoneCechUnit, isInducing_stoneCechUnit, separatesPoints_continuous_of_t35Space, separatesPoints_continuous_of_t35Space_Icc, t35Space_iff, t35Space_iff_isEmbedding_stoneCechUnit	32
Total	34

CompletelyRegularSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completely_regular 📖	mathematical	Set Set.instMembership	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.EqOn Pi.instOne Set.Icc.instOne	—	—
completely_regular_isOpen 📖	mathematical	IsOpen Set Set.instMembership	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.EqOn Pi.instOne Set.Icc.instOne Compl.compl Set.instCompl	—	Real.instIsOrderedRing completelyRegularSpace_iff_isOpen
instRegularSpace 📖	mathematical	—	RegularSpace	—	regularSpace_iff Real.instIsOrderedRing completely_regular Filter.disjoint_of_map Disjoint.mono Continuous.tendsto_nhdsSet_nhds Continuous.continuousAt disjoint_nhds_nhds instT2SpaceSubtype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace zero_ne_one NeZero.one unitInterval.instNontrivialElemReal
isTopologicalBasis_clopens_of_cardinalMk_lt_continuum 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.continuum	TopologicalSpace.IsTopologicalBasis setOf Set IsClopen	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds IsClopen.isOpen Real.instIsOrderedRing Cardinal.lift_uzero Cardinal.lift_continuum LE.le.trans_lt Cardinal.mk_range_le_lift Cardinal.lift_strictMono unitInterval.eq_1 Cardinal.mk_Icc_real zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Cardinal.lift_lt Set.ext IsClosed.preimage isClosed_Iic instClosedIicTopology Subtype.instOrderClosedTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal IsOpen.preimage isOpen_Iio instClosedIciTopology Set.preimage_subset_iff Mathlib.Tactic.Contrapose.contrapose₁ unitInterval.le_one' completely_regular_isOpen

NormalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompletelyRegularSpace 📖	mathematical	—	CompletelyRegularSpace	—	Real.instIsOrderedRing completelyRegularSpace_iff isClosed_closure Set.disjoint_iff Specializes.mem_closed Specializes.symm specializes_iff_mem_closure exists_continuous_zero_one_of_isClosed subset_closure Set.mem_singleton

T35Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instT3space 📖	mathematical	—	T3Space	—	toT0Space CompletelyRegularSpace.instRegularSpace toCompletelyRegularSpace
toCompletelyRegularSpace 📖	mathematical	—	CompletelyRegularSpace	—	—
toT0Space 📖	mathematical	—	T0Space	—	—

T4Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instT35Space 📖	mathematical	—	T35Space	—	T3Space.toT0Space t3Space NormalSpace.instCompletelyRegularSpace toNormalSpace instR0Space instR1Space T3Space.toRegularSpace

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
t35Space 📖	mathematical	Topology.IsEmbedding	T35Space	—	t0Space T35Space.toT0Space Topology.IsInducing.completelyRegularSpace T35Space.toCompletelyRegularSpace isInducing

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completelyRegularSpace 📖	mathematical	Topology.IsInducing	CompletelyRegularSpace	—	Real.instIsOrderedRing isClosed_iff CompletelyRegularSpace.completely_regular Set.mem_preimage Continuous.comp continuous Set.EqOn.comp_right Set.mapsTo_preimage

(root)

Definitions

Name	Category	Theorems
CompletelyRegularSpace 📖	CompData	14 math math: completelyRegularSpace_iff_isOpen, UniformSpace.toCompletelyRegularSpace, instCompletelyRegularSpaceSubtype, Topology.IsInducing.completelyRegularSpace, T35Space.toCompletelyRegularSpace, instCompletelyRegularSpaceProd, NormalSpace.instCompletelyRegularSpace, completelyRegularSpace_induced, CompletelyRegularSpace.of_exists_uniformSpace, completelyRegularSpace_inf, t35Space_iff, completelyRegularSpace_iff_isInducing_stoneCechUnit, completelyRegularSpace_iff, completelyRegularSpace_iff_exists_uniformSpace
T35Space 📖	CompData	6 math math: Topology.IsEmbedding.t35Space, t35Space_iff_isEmbedding_stoneCechUnit, instT35SpaceSubtype, t35Space_iff, instT35SpaceProd, T4Space.instT35Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completelyRegularSpace_iInf 📖	mathematical	CompletelyRegularSpace	iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	Real.instIsOrderedRing completelyRegularSpace_iff_isOpen nhds_iInf IsOpen.mem_nhds_iff CompletelyRegularSpace.completely_regular_isOpen ZeroLEOneClass.factZeroLeOne Real.instZeroLEOneClass Continuous.finset_sup TopologicalLattice.toContinuousSup LinearOrder.topologicalLattice Subtype.instOrderClosedTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_iInf_dom Finset.sup_apply Set.compl_iInter unitInterval.instNontrivialElemReal
completelyRegularSpace_iff 📖	mathematical	—	CompletelyRegularSpace Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.EqOn Pi.instOne Set.Icc.instOne	—	Real.instIsOrderedRing
completelyRegularSpace_iff_isInducing_stoneCechUnit 📖	mathematical	—	CompletelyRegularSpace Topology.IsInducing StoneCech instTopologicalSpaceStoneCech stoneCechUnit	—	isInducing_stoneCechUnit Topology.IsInducing.completelyRegularSpace NormalSpace.instCompletelyRegularSpace NormalSpace.of_regularSpace_lindelofSpace instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instWeaklyLocallyCompactSpaceOfCompactSpace instCompactSpaceStoneCech T2Space.r1Space instT2SpaceStoneCech instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact instR0Space
completelyRegularSpace_iff_isOpen 📖	mathematical	—	CompletelyRegularSpace Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.EqOn Pi.instOne Set.Icc.instOne Compl.compl Set.instCompl	—	Real.instIsOrderedRing Function.Surjective.forall compl_surjective
completelyRegularSpace_induced 📖	mathematical	—	CompletelyRegularSpace TopologicalSpace.induced	—	Topology.IsInducing.completelyRegularSpace Topology.IsInducing.induced
completelyRegularSpace_inf 📖	mathematical	—	CompletelyRegularSpace TopologicalSpace SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	inf_eq_iInf completelyRegularSpace_iInf
injective_stoneCechUnit_of_t35Space 📖	mathematical	—	StoneCech stoneCechUnit	—	Mathlib.Tactic.Contrapose.contrapose₁ separatesPoints_continuous_of_t35Space_Icc eq_if_stoneCechUnit_eq instT2SpaceSubtype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal
instCompletelyRegularSpaceForall 📖	mathematical	CompletelyRegularSpace	Pi.topologicalSpace	—	completelyRegularSpace_iInf completelyRegularSpace_induced
instCompletelyRegularSpaceProd 📖	mathematical	—	CompletelyRegularSpace instTopologicalSpaceProd	—	completelyRegularSpace_inf completelyRegularSpace_induced
instCompletelyRegularSpaceSubtype 📖	mathematical	—	CompletelyRegularSpace instTopologicalSpaceSubtype	—	Topology.IsInducing.completelyRegularSpace Topology.IsInducing.subtypeVal
instT35SpaceForall 📖	mathematical	T35Space	Pi.topologicalSpace	—	Pi.instT0Space T35Space.toT0Space instCompletelyRegularSpaceForall T35Space.toCompletelyRegularSpace
instT35SpaceProd 📖	mathematical	—	T35Space instTopologicalSpaceProd	—	Prod.instT0Space T35Space.toT0Space instCompletelyRegularSpaceProd T35Space.toCompletelyRegularSpace
instT35SpaceSubtype 📖	mathematical	—	T35Space instTopologicalSpaceSubtype	—	Subtype.t0Space T35Space.toT0Space instCompletelyRegularSpaceSubtype T35Space.toCompletelyRegularSpace
isDenseEmbedding_stoneCechUnit 📖	mathematical	—	IsDenseEmbedding StoneCech instTopologicalSpaceStoneCech stoneCechUnit	—	isDenseInducing_stoneCechUnit T35Space.toCompletelyRegularSpace injective_stoneCechUnit_of_t35Space
isDenseInducing_stoneCechUnit 📖	mathematical	—	IsDenseInducing StoneCech instTopologicalSpaceStoneCech stoneCechUnit	—	isInducing_stoneCechUnit denseRange_stoneCechUnit
isEmbedding_stoneCechUnit 📖	mathematical	—	Topology.IsEmbedding StoneCech instTopologicalSpaceStoneCech stoneCechUnit	—	isInducing_stoneCechUnit T35Space.toCompletelyRegularSpace injective_stoneCechUnit_of_t35Space
isInducing_stoneCechUnit 📖	mathematical	—	Topology.IsInducing StoneCech instTopologicalSpaceStoneCech stoneCechUnit	—	Topology.isInducing_iff_nhds le_antisymm Filter.map_le_iff_le_comap Continuous.continuousAt continuous_stoneCechUnit Filter.HasBasis.mem_iff Filter.HasBasis.comap nhds_basis_opens Real.instIsOrderedRing CompletelyRegularSpace.completely_regular_isOpen instT2SpaceSubtype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Set.mem_preimage stoneCechExtend_stoneCechUnit Set.mem_compl_iff Set.mem_singleton_iff NeZero.one unitInterval.instNontrivialElemReal IsOpen.preimage continuous_stoneCechExtend isOpen_compl_singleton Subtype.t1Space T5Space.toT1Space OrderTopology.t5Space Set.preimage_comp stoneCechExtend_extends Set.preimage_compl Set.compl_subset_comm
separatesPoints_continuous_of_t35Space 📖	mathematical	—	Set.SeparatesPoints Real setOf Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Real.instIsOrderedRing CompletelyRegularSpace.completely_regular T35Space.toCompletelyRegularSpace isClosed_singleton T2Space.t1Space T25Space.t2Space T3Space.t25Space T35Space.instT3space Continuous.comp continuous_subtype_val NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
separatesPoints_continuous_of_t35Space_Icc 📖	mathematical	—	Set.SeparatesPoints Set.Elem Real unitInterval setOf Continuous instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Real.instIsOrderedRing CompletelyRegularSpace.completely_regular T35Space.toCompletelyRegularSpace isClosed_singleton T2Space.t1Space T25Space.t2Space T3Space.t25Space T35Space.instT3space NeZero.one unitInterval.instNontrivialElemReal
t35Space_iff 📖	mathematical	—	T35Space T0Space CompletelyRegularSpace	—	—
t35Space_iff_isEmbedding_stoneCechUnit 📖	mathematical	—	T35Space Topology.IsEmbedding StoneCech instTopologicalSpaceStoneCech stoneCechUnit	—	isEmbedding_stoneCechUnit Topology.IsEmbedding.t35Space T4Space.instT35Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space instT2SpaceStoneCech NormalSpace.of_regularSpace_lindelofSpace instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instWeaklyLocallyCompactSpaceOfCompactSpace instCompactSpaceStoneCech T2Space.r1Space instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact

---

← Back to Index