Completion

📁 Source: Mathlib/Analysis/InnerProductSpace/Completion.lean

Statistics

Metric	Count
Definitions instInner, instInnerProductSpace, innerProductSpace, toInner	4
Theorems inner_eq_inner, inner_mk_mk, inner, continuous_inner, inner_coe	5
Total	9

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_eq_inner 📖	mathematical	Inseparable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Inner.inner InnerProductSpace.toInner	—	eq T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity map prod continuous_inner

SeparationQuotient

Definitions

Name	Category	Theorems
instInner 📖	CompOp	1 math math: inner_mk_mk
instInnerProductSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_mk_mk 📖	mathematical	—	Inner.inner SeparationQuotient UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instInner InnerProductSpace.toInner	—	—

UniformSpace.Completion

Definitions

Name	Category	Theorems
innerProductSpace 📖	CompOp	3 math math: PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, PositiveLinearMap.gnsStarAlgHom_apply, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply
toInner 📖	CompOp	3 math math: Continuous.inner, inner_coe, continuous_inner

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_inner 📖	mathematical	—	Continuous UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace uniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner toInner InnerProductSpace.toInner	—	Algebra.to_smulCommClass AddMonoidHom.ext inner_zero_left inner_add_left continuous_inner toInner.eq_1 Inner.inner.eq_1 IsDenseInducing.extend_Z_bilin SeminormedAddCommGroup.to_isUniformAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup isDenseInducing_toCompl T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity RCLike.toCompleteSpace
inner_coe 📖	mathematical	—	Inner.inner UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace toInner UniformSpace.toTopologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toInner coe'	—	IsDenseInducing.extend_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsDenseInducing.prodMap isDenseInducing_coe continuous_inner

UniformSpace.Completion.Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	Continuous UniformSpace.Completion PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniformSpace.toTopologicalSpace UniformSpace.Completion.uniformSpace	SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner UniformSpace.Completion.toInner InnerProductSpace.toInner	—	Continuous.comp UniformSpace.Completion.continuous_inner Continuous.prodMk

---

← Back to Index