Continuous

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

Statistics

Metric	Count
Definitions	0
Theorems inner, inner, inner, inner, eq_of_inner_left, eq_of_inner_right, eq_zero_of_inner_left, eq_zero_of_inner_right, eq_of_inner_left, eq_of_inner_right, eq_zero_of_inner_left, eq_zero_of_inner_right, inner, continuous_inner, isBoundedBilinearMap_inner	15
Total	15

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner InnerProductSpace.toInner	—	Filter.Tendsto.inner

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_inner_left 📖	—	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Inner.inner InnerProductSpace.toInner	—	—	sub_eq_zero eq_zero_of_inner_left inner_sub_left
eq_of_inner_right 📖	—	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Inner.inner InnerProductSpace.toInner	—	—	sub_eq_zero eq_zero_of_inner_right inner_sub_right
eq_zero_of_inner_left 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	mono Submodule.subset_span Continuous.ext_on TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.inner continuous_const continuous_id Submodule.span_induction inner_zero_right inner_add_right add_zero inner_smul_right MulZeroClass.mul_zero inner_self_eq_norm_sq_to_K isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat IsSimpleRing.instNontrivial DivisionRing.isSimpleRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
eq_zero_of_inner_right 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	eq_zero_of_inner_left Mathlib.Tactic.DepRewrite.nddcongrArg inner_conj_symm map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_inner_left 📖	—	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Inner.inner InnerProductSpace.toInner	—	—	Dense.eq_of_inner_left
eq_of_inner_right 📖	—	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Inner.inner InnerProductSpace.toInner	—	—	Dense.eq_of_inner_right
eq_zero_of_inner_left 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Dense.eq_zero_of_inner_left
eq_zero_of_inner_right 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Inner.inner InnerProductSpace.toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Dense.eq_zero_of_inner_right

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Filter.Tendsto Inner.inner InnerProductSpace.toInner nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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 IsScalarTower.restrictScalars
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