Extend

📁 Source: Mathlib/Analysis/Normed/Operator/Extend.lean

Statistics

Metric	Count
Definitions extend, extend, extendOfIsometry, compLeftInverse, extendOfNorm	5
Theorems extend_eq, extend_unique, extend_zero, opNorm_extend_le, extendOfIsometry_apply, extendOfIsometry_eq, extendOfIsometry_symm_apply, extendOfIsometry_symm_eq, extend_apply, extend_eq, extend_symm_apply, extend_symm_eq, norm_extend_le, norm_extend_symm_le, compLeftInverse_apply_of_bdd, extendOfNorm_eq, extendOfNorm_unique, norm_extendOfNorm_apply_le, opNorm_extendOfNorm_le	19
Total	24

ContinuousLinearMap

Definitions

Name	Category	Theorems
extend 📖	CompOp	4 math math: opNorm_extend_le, extend_zero, extend_unique, extend_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extend_eq 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike IsUniformInducing	extend	—	IsDenseInducing.extend_eq T25Space.t2Space T3Space.t25Space instT3Space IsTopologicalAddGroup.regularSpace IsUniformAddGroup.to_topologicalAddGroup IsUniformInducing.isDenseInducing cont
extend_unique 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike IsUniformInducing comp RingHomCompTriple.ids	extend	—	RingHomCompTriple.ids coeFn_injective uniformly_extend_unique ext_iff continuous
extend_zero 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid funLike IsUniformInducing	extend zero	—	extend_unique zero_comp RingHomCompTriple.ids
opNorm_extend_le 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Real.instMul NNReal.toReal	AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup hasOpNorm extend SeminormedAddCommGroup.to_isUniformAddGroup T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity EMetricSpace.toPseudoEMetricSpace IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	opNorm_le_bound SeminormedAddCommGroup.to_isUniformAddGroup T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul le_total mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg norm_le_zero_iff LE.le.trans mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono norm_zero MulZeroClass.mul_zero Unique.instSubsingleton isClosed_property isClosed_le OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.norm cont Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const extend_eq IsUniformEmbedding.isUniformInducing isUniformEmbedding_of_bound le_opNorm mul_le_mul_of_nonneg_left mul_comm mul_assoc le_refl

LinearEquiv

Definitions

Name	Category	Theorems
extend 📖	CompOp	6 math math: norm_extend_le, extend_eq, extend_symm_apply, extend_symm_eq, norm_extend_symm_le, extend_apply
extendOfIsometry 📖	CompOp	4 math math: extendOfIsometry_symm_eq, extendOfIsometry_symm_apply, extendOfIsometry_apply, extendOfIsometry_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendOfIsometry_apply 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule LinearMap.instFunLike Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	LinearIsometryEquiv LinearIsometryEquiv.instEquivLike extendOfIsometry ContinuousLinearMap DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike LinearMap.extendOfNorm NormedSpace.toIsBoundedSMul LinearMap.comp RingHomCompTriple.right_ids toLinearMap	—	—
extendOfIsometry_eq 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule LinearMap.instFunLike Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	LinearIsometryEquiv LinearIsometryEquiv.instEquivLike extendOfIsometry	—	LinearMap.extendOfNorm_eq NormedSpace.toIsBoundedSMul one_mul
extendOfIsometry_symm_apply 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule LinearMap.instFunLike Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	LinearIsometryEquiv LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm extendOfIsometry ContinuousLinearMap DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike LinearMap.extendOfNorm NormedSpace.toIsBoundedSMul LinearMap.comp RingHomCompTriple.right_ids toLinearMap symm	—	—
extendOfIsometry_symm_eq 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule LinearMap.instFunLike Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv	LinearIsometryEquiv LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm extendOfIsometry symm	—	apply_symm_apply LinearMap.extendOfNorm_eq NormedSpace.toIsBoundedSMul one_mul
extend_apply 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Real.instMul symm	ContinuousLinearEquiv ContinuousLinearEquiv.equivLike extend ContinuousLinearMap SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike LinearMap.extendOfNorm LinearMap.comp RingHomCompTriple.right_ids toLinearMap	—	—
extend_eq 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Real.instMul symm	ContinuousLinearEquiv ContinuousLinearEquiv.equivLike extend	—	LinearMap.extendOfNorm_eq
extend_symm_apply 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Real.instMul symm	ContinuousLinearEquiv ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm extend ContinuousLinearMap SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap.funLike LinearMap.extendOfNorm LinearMap.comp RingHomCompTriple.right_ids toLinearMap	—	—
extend_symm_eq 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Real.instMul symm	ContinuousLinearEquiv ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm extend	—	LinearMap.extendOfNorm_eq
norm_extend_le 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Real.instMul symm	ContinuousLinearEquiv ContinuousLinearEquiv.equivLike extend	—	LinearMap.norm_extendOfNorm_apply_le
norm_extend_symm_le 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm LinearEquiv EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Real.instMul symm	ContinuousLinearEquiv ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm extend	—	LinearMap.norm_extendOfNorm_apply_le

LinearMap

Definitions

Name	Category	Theorems
compLeftInverse 📖	CompOp	1 math math: compLeftInverse_apply_of_bdd
extendOfNorm 📖	CompOp	8 math math: LinearEquiv.extendOfIsometry_symm_apply, LinearEquiv.extendOfIsometry_apply, extendOfNorm_eq, LinearEquiv.extend_symm_apply, opNorm_extendOfNorm_le, extendOfNorm_unique, norm_extendOfNorm_apply_le, LinearEquiv.extend_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compLeftInverse_apply_of_bdd 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instFunLike Real.instMul SeminormedAddCommGroup.toNorm RingHom.id Semiring.toNonAssocSemiring SeminormedAddCommGroup.toAddCommGroup	ContinuousLinearMap Submodule SetLike.instMembership Submodule.setLike range RingHomSurjective.ids instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike compLeftInverse	—	RingHomSurjective.ids quotKerEquivRange_symm_apply_image
extendOfNorm_eq 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm ESeminormedAddCommMonoid.toAddCommMonoid NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instMul SeminormedAddCommGroup.toNorm	ContinuousLinearMap ContinuousLinearMap.funLike extendOfNorm	—	RingHomSurjective.ids SeminormedAddCommGroup.to_isUniformAddGroup T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul ContinuousLinearMap.extend_eq IsUniformEmbedding.isUniformInducing isUniformEmbedding_subtype_val mem_range_self compLeftInverse_apply_of_bdd
extendOfNorm_unique 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm ESeminormedAddCommMonoid.toAddCommMonoid NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instMul SeminormedAddCommGroup.toNorm comp RingHomCompTriple.ids ContinuousLinearMap.toLinearMap	extendOfNorm	—	RingHomCompTriple.ids ContinuousLinearMap.extend_unique IsUniformEmbedding.isUniformInducing isUniformEmbedding_subtype_val ContinuousLinearMap.ext RingHomSurjective.ids compLeftInverse_apply_of_bdd
norm_extendOfNorm_apply_le 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instFunLike Real Real.instLE Norm.norm NormedAddCommGroup.toNorm ESeminormedAddCommMonoid.toAddCommMonoid NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instMul SeminormedAddCommGroup.toNorm	ContinuousLinearMap ContinuousLinearMap.funLike extendOfNorm	—	RingHomSurjective.ids extendOfNorm_eq Dense.induction isClosed_le OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.norm ContinuousLinearMap.continuous Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fst continuous_id' Continuous.snd Continuous.prodMk continuous_const
opNorm_extendOfNorm_le 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule instFunLike Real Real.instLE Real.instZero Norm.norm NormedAddCommGroup.toNorm ESeminormedAddCommMonoid.toAddCommMonoid NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.instMul SeminormedAddCommGroup.toNorm	ContinuousLinearMap DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing ContinuousLinearMap.hasOpNorm extendOfNorm NormedSpace.toIsBoundedSMul	—	ContinuousLinearMap.opNorm_le_bound NormedSpace.toIsBoundedSMul norm_extendOfNorm_apply_le

---

← Back to Index