CompletelyMetrizable

📁 Source: Mathlib/Topology/Metrizable/CompletelyMetrizable.lean

Statistics

Metric	Count
Definitions IsCompletelyMetrizableSpace, IsCompletelyPseudoMetrizableSpace, UpgradedIsCompletelyMetrizableSpace, toMetricSpace, UpgradedIsCompletelyPseudoMetrizableSpace, toPseudoMetricSpace, completelyMetrizableMetric, completelyPseudoMetrizableMetric, upgradeIsCompletelyMetrizable, upgradeIsCompletelyPseudoMetrizable	10
Theorems isCompletelyMetrizableSpace, isCompletelyPseudoMetrizableSpace, toIsCompletelyMetrizableSpace, toIsCompletelPseudoMetrizableSpace, complete, discrete, of_completeSpace_metrizable, pi_countable, prod, sigma, sum, toIsCompletelyPseudoMetrizableSpace, univ, IsCompletelyMetrizableSpace_of_isCompletelyPseudoMetrizableSpace, PseudoMetrizableSpace, complete, of_completeSpace_pseudometrizable, pi_countable, prod, sum, toCompleteSpace, toCompleteSpace, complete_completelyMetrizableMetric, complete_completelyPseudoMetrizableMetric, IsCompletelyMetrizableSpace, IsCompletelyPseudoMetrizableSpace	26
Total	36

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompletelyMetrizableSpace 📖	mathematical	—	TopologicalSpace.IsCompletelyMetrizableSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsClosedEmbedding.IsCompletelyMetrizableSpace isClosedEmbedding_subtypeVal
isCompletelyPseudoMetrizableSpace 📖	mathematical	—	TopologicalSpace.IsCompletelyPseudoMetrizableSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsClosedEmbedding.IsCompletelyPseudoMetrizableSpace isClosedEmbedding_subtypeVal

MetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsCompletelyMetrizableSpace 📖	mathematical	—	TopologicalSpace.IsCompletelyMetrizableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toPseudoMetricSpace	—	—

PseudoMetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsCompletelPseudoMetrizableSpace 📖	mathematical	—	TopologicalSpace.IsCompletelyPseudoMetrizableSpace UniformSpace.toTopologicalSpace toUniformSpace	—	—

TopologicalSpace

Definitions

Name	Category	Theorems
IsCompletelyMetrizableSpace 📖	CompData	10 math math: MetricSpace.toIsCompletelyMetrizableSpace, IsCompletelyMetrizableSpace.prod, PolishSpace.toIsCompletelyMetrizableSpace, IsClosed.isCompletelyMetrizableSpace, IsCompletelyMetrizableSpace.sum, IsCompletelyMetrizableSpace.discrete, IsCompletelyMetrizableSpace.of_completeSpace_metrizable, Topology.IsClosedEmbedding.IsCompletelyMetrizableSpace, IsCompletelyMetrizableSpace.univ, IsCompletelyMetrizableSpace_of_isCompletelyPseudoMetrizableSpace
IsCompletelyPseudoMetrizableSpace 📖	CompData	7 math math: IsClosed.isCompletelyPseudoMetrizableSpace, Topology.IsClosedEmbedding.IsCompletelyPseudoMetrizableSpace, PseudoMetricSpace.toIsCompletelPseudoMetrizableSpace, IsCompletelyPseudoMetrizableSpace.prod, IsCompletelyPseudoMetrizableSpace.of_completeSpace_pseudometrizable, IsCompletelyPseudoMetrizableSpace.sum, IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace
UpgradedIsCompletelyMetrizableSpace 📖	CompData	—
UpgradedIsCompletelyPseudoMetrizableSpace 📖	CompData	—
completelyMetrizableMetric 📖	CompOp	1 math math: complete_completelyMetrizableMetric
completelyPseudoMetrizableMetric 📖	CompOp	1 math math: complete_completelyPseudoMetrizableMetric
upgradeIsCompletelyMetrizable 📖	CompOp	—
upgradeIsCompletelyPseudoMetrizable 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsCompletelyMetrizableSpace_of_isCompletelyPseudoMetrizableSpace 📖	mathematical	—	IsCompletelyMetrizableSpace	—	UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace
complete_completelyMetrizableMetric 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace completelyMetrizableMetric	—	IsCompletelyMetrizableSpace.complete MetricSpace.replaceTopology_eq
complete_completelyPseudoMetrizableMetric 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace completelyPseudoMetrizableMetric	—	IsCompletelyPseudoMetrizableSpace.complete PseudoMetricSpace.replaceTopology_eq

TopologicalSpace.IsCompletelyMetrizableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complete 📖	mathematical	—	UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace CompleteSpace	—	—
discrete 📖	mathematical	—	TopologicalSpace.IsCompletelyMetrizableSpace	—	eq_or_ne add_zero zero_add Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le ENNReal.coe_nnreal_eq NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing DiscreteTopology.eq_bot eq_bot_of_singletons_open subset_antisymm Set.instAntisymmSubset Set.singleton_subset_iff Metric.mem_ball_self Metric.isOpen_ball Metric.complete_of_cauchySeq_tendsto Metric.cauchySeq_iff' tendsto_atTop_of_eventually_const
of_completeSpace_metrizable 📖	mathematical	—	TopologicalSpace.IsCompletelyMetrizableSpace UniformSpace.toTopologicalSpace	—	—
pi_countable 📖	mathematical	TopologicalSpace.IsCompletelyMetrizableSpace	Pi.topologicalSpace	—	of_completeSpace_metrizable Pi.complete TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace instIsCountablyGeneratedProdForallUniformityOfCountable EMetric.instIsCountablyGeneratedUniformity Pi.instT0Space T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity
prod 📖	mathematical	—	TopologicalSpace.IsCompletelyMetrizableSpace instTopologicalSpaceProd	—	of_completeSpace_metrizable CompleteSpace.prod TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace instIsCountablyGeneratedProdUniformity EMetric.instIsCountablyGeneratedUniformity Prod.instT0Space T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity
sigma 📖	mathematical	TopologicalSpace.IsCompletelyMetrizableSpace	instTopologicalSpaceSigma	—	of_completeSpace_metrizable Metric.Sigma.completeSpace TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace EMetric.instIsCountablyGeneratedUniformity T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space Sigma.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity
sum 📖	mathematical	—	TopologicalSpace.IsCompletelyMetrizableSpace instTopologicalSpaceSum	—	of_completeSpace_metrizable CompleteSpace.sum TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace instIsCountablyGeneratedProdSumUniformity EMetric.instIsCountablyGeneratedUniformity T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space instT2SpaceSum TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity
toIsCompletelyPseudoMetrizableSpace 📖	mathematical	—	TopologicalSpace.IsCompletelyPseudoMetrizableSpace	—	—
univ 📖	mathematical	—	TopologicalSpace.IsCompletelyMetrizableSpace Set.Elem Set.univ instTopologicalSpaceSubtype Set Set.instMembership	—	IsClosed.isCompletelyMetrizableSpace isClosed_univ

TopologicalSpace.IsCompletelyPseudoMetrizableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
PseudoMetrizableSpace 📖	mathematical	—	TopologicalSpace.PseudoMetrizableSpace	—	PseudoEMetricSpace.pseudoMetrizableSpace
complete 📖	mathematical	—	UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace CompleteSpace	—	—
of_completeSpace_pseudometrizable 📖	mathematical	—	TopologicalSpace.IsCompletelyPseudoMetrizableSpace UniformSpace.toTopologicalSpace	—	—
pi_countable 📖	mathematical	TopologicalSpace.IsCompletelyPseudoMetrizableSpace	Pi.topologicalSpace	—	of_completeSpace_pseudometrizable Pi.complete TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace instIsCountablyGeneratedProdForallUniformityOfCountable EMetric.instIsCountablyGeneratedUniformity
prod 📖	mathematical	—	TopologicalSpace.IsCompletelyPseudoMetrizableSpace instTopologicalSpaceProd	—	of_completeSpace_pseudometrizable CompleteSpace.prod TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace instIsCountablyGeneratedProdUniformity EMetric.instIsCountablyGeneratedUniformity
sum 📖	mathematical	—	TopologicalSpace.IsCompletelyPseudoMetrizableSpace instTopologicalSpaceSum	—	of_completeSpace_pseudometrizable CompleteSpace.sum TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace instIsCountablyGeneratedProdSumUniformity EMetric.instIsCountablyGeneratedUniformity

TopologicalSpace.UpgradedIsCompletelyMetrizableSpace

Definitions

Name	Category	Theorems
toMetricSpace 📖	CompOp	1 math math: toCompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCompleteSpace 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace toMetricSpace	—	—

TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace

Definitions

Name	Category	Theorems
toPseudoMetricSpace 📖	CompOp	1 math math: toCompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCompleteSpace 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace toPseudoMetricSpace	—	—

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsCompletelyMetrizableSpace 📖	mathematical	Topology.IsClosedEmbedding	TopologicalSpace.IsCompletelyMetrizableSpace	—	isEmbedding Topology.IsEmbedding.toIsInducing completeSpace_iff_isComplete_range Isometry.isUniformInducing Topology.IsEmbedding.to_isometry IsClosed.isComplete TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace isClosed_range TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable EMetric.instIsCountablyGeneratedUniformity T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity
IsCompletelyPseudoMetrizableSpace 📖	mathematical	Topology.IsClosedEmbedding	TopologicalSpace.IsCompletelyPseudoMetrizableSpace	—	Topology.IsEmbedding.toIsInducing isEmbedding completeSpace_iff_isComplete_range Isometry.isUniformInducing Topology.IsEmbedding.to_isometry IsClosed.isComplete TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace isClosed_range TopologicalSpace.IsCompletelyPseudoMetrizableSpace.of_completeSpace_pseudometrizable EMetric.instIsCountablyGeneratedUniformity

---

← Back to Index