Continuous

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

Statistics

Metric	Count
Definitions	0
Theorems inner, inner, inner, inner, inner, continuous_inner, isBoundedBilinearMap_inner	7
Total	7

Continuous

Theorems

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

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner	—	Filter.Tendsto.inner

ContinuousOn

Theorems

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

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner	—	Filter.Tendsto.inner

Filter.Tendsto

Theorems

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

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_inner 📖	mathematical	—	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner	—	IsBoundedBilinearMap.continuous isBoundedBilinearMap_inner RestrictScalars.isScalarTower
isBoundedBilinearMap_inner 📖	mathematical	—	IsBoundedBilinearMap Real Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	inner_add_left algebraMap_smul inner_smul_real_left inner_add_right inner_smul_real_right zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike one_mul norm_inner_le_norm

---

← Back to Index