NormedSpace

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

Statistics

Metric	Count
Definitions toNormedAddCommGroup, toNormedRing, IsCoercive, inl, inr, postcomp, single	7
Theorems antilipschitz, coord_norm, nnnorm_symm_pos, norm_pos, norm_symm_pos, one_le_norm_mul_norm_symm, subsingleton_or_nnnorm_symm_pos, subsingleton_or_norm_symm_pos, antilipschitz_of_isEmbedding, norm_inl, norm_inl_le_one, norm_inr, norm_inr_le_one, norm_single, norm_single_le_one, norm_smulRightL, norm_smulRightL_le, opNorm_comp_linearIsometryEquiv, opNorm_zero_iff, enorm_toContinuousLinearMap, inl_apply, inr_apply, nnnorm_toContinuousLinearMap, norm_toContinuousLinearMap, norm_toContinuousLinearMap_comp, antilipschitz_of_comap_nhds_le, bound_of_ball_bound, bound_of_shell, equicontinuous_TFAE, norm_subtypeL	30
Total	37

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz 📖	mathematical	—	AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup toContinuousLinearMap symm DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike equivLike	—	LipschitzWith.to_rightInverse lipschitz LinearEquiv.left_inv
coord_norm 📖	mathematical	—	Norm.norm StrongDual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Submodule ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.hasOpNorm Submodule.seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing Submodule.normedSpace Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction NormedField.toNormedSpace RingHom.id Semiring.toNonAssocSemiring coord Real Real.instInv NormedAddCommGroup.toNorm	—	norm_pos_iff ContinuousLinearMap.homothety_norm IsScalarTower.left RingHomIsometric.ids EMetric.instNontrivialTopologyOfNontrivial Submodule.nontrivial_span_singleton homothety_inverse RingHomInvPair.ids DivisionRing.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LinearEquiv.toSpanNonzeroSingleton_homothety NormedSpace.toNormSMulClass
nnnorm_symm_pos 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup toContinuousLinearMap symm	—	norm_symm_pos
norm_pos 📖	mathematical	—	Real Real.instLT Real.instZero Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.hasOpNorm toContinuousLinearMap	—	pos_of_mul_pos_left MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_lt_of_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero one_le_norm_mul_norm_symm norm_nonneg
norm_symm_pos 📖	mathematical	—	Real Real.instLT Real.instZero Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.hasOpNorm toContinuousLinearMap symm	—	pos_of_mul_pos_right PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero one_le_norm_mul_norm_symm norm_nonneg
one_le_norm_mul_norm_symm 📖	mathematical	—	Real Real.instLE Real.instOne Real.instMul Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.hasOpNorm toContinuousLinearMap symm	—	mul_comm RingHomInvPair.triples₂ coe_symm_comp_coe ContinuousLinearMap.norm_id EMetric.instNontrivialTopologyOfNontrivial ContinuousLinearMap.opNorm_comp_le
subsingleton_or_nnnorm_symm_pos 📖	mathematical	—	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup toContinuousLinearMap symm	—	subsingleton_or_norm_symm_pos
subsingleton_or_norm_symm_pos 📖	mathematical	—	Real Real.instLT Real.instZero Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.hasOpNorm toContinuousLinearMap symm	—	subsingleton_or_nontrivial norm_symm_pos

ContinuousLinearMap

Definitions

Name	Category	Theorems
toNormedAddCommGroup 📖	CompOp	234 math math: ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, SchwartzMap.lineDerivOpCLM_eq, Bundle.ContMDiffRiemannianMetric.contMDiff, MDifferentiableOn.clm_postcomp, Real.fderiv_fourierIntegral, ContDiff.fderiv_succ, ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap, MDifferentiableAt.cle_arrowCongr, hasFTaylorSeriesUpToOn_top_iff_right, hasFDerivAt_integral_of_dominated_loc_of_lip_interval, integral_apply, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, Real.fourier_continuousLinearMap_apply, ContDiffAt.fderiv_right_succ, iteratedFDerivWithin_succ_eq_comp_right, norm_iteratedFDerivWithin_clm_apply, ContMDiffWithinAt.mfderivWithin_const, ContMDiffOn.clm_postcomp, FormalMultilinearSeries.derivSeries_coeff_one, mdifferentiableOn_symm_coordChangeL, ContDiffMapSupportedIn.fderivLM_eq_of_scalars, fderiv_clm_comp, ContDiffMapSupportedIn.seminorm_fderivLM_le, ContDiffMapSupportedIn.seminorm_fderivLM_top, Bundle.ContinuousLinearMap.vectorBundle, norm_iteratedFDeriv_clm_apply, SchwartzMap.fderivCLM_apply, HasFDerivAt.norm_sq, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, ContDiffAt.fderiv_succ, VectorBundleCore.contMDiffOn_coordChange, MDifferentiable.clm_postcomp, HasFPowerSeriesWithinOnBall.fderivWithin, ContDiffMapSupportedIn.fderivCLM_apply_of_gt, TestFunction.fderivCLM_apply_of_le, MDifferentiable.cle_arrowCongr, TestFunction.fderivCLM_ofSupportedIn, Real.fderiv_fourier, MeasureTheory.L1.setToL1_smul_left, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, VectorFourier.fourierIntegral_continuousLinearMap_apply, norm_iteratedFDerivWithin_clm_apply_const, DoubleCentralizer.norm_def, contDiff_succ_iff_fderiv, MDifferentiableAt.clm_prodMap, MDifferentiableAt.clm_postcomp, ContDiffWithinAt.hasFDerivWithinAt_nhds, VectorFourier.hasFDerivAt_fourierIntegral, MeasureTheory.convolution_precompR_apply, Bundle.ContinuousRiemannianMetric.continuous, DoubleCentralizer.nnnorm_def, iteratedFDerivWithin_succ_apply_right, contDiffAt_map_inverse, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, Real.fourierIntegral_continuousLinearMap_apply, AnalyticOn.fderivWithin, ContDiffAt.fderiv_right, ContMDiffFiberwiseLinear.locality_aux₂, MDifferentiableWithinAt.cle_arrowCongr, MDifferentiableWithinAt.clm_precomp, ContMDiffVectorBundle.continuousLinearMap, ContDiffOn.fderiv_of_isOpen, inCoordinates_apply_eq₂, AnalyticOnNhd.fderiv_of_isOpen, contDiffOn_infty_iff_fderivWithin, Real.hasFDerivAt_fourier, HasFPowerSeriesOnBall.fderiv, ContMDiffOn.clm_precomp, ContMDiffOn.coordChangeL, mdifferentiableAt_hom_bundle, LinearMap.IsSymmetric.coe_toSelfAdjoint, MeasureTheory.hasFDerivAt_convolution_right_with_param, ContMDiffAt.mfderiv_const, HasCompactSupport.hasFDerivAt_convolution_right, Differentiable.fderiv_two, MDifferentiableOn.coordChangeL, IsContMDiffRiemannianBundle.exists_contMDiff, ContDiffWithinAt.fderivWithin'', ContMDiffOn.cle_arrowCongr, MDifferentiableOn.clm_prodMap, contMDiffAt_coordChangeL, hasFDerivAt_integral_of_dominated_loc_of_lip', MDifferentiableWithinAt.coordChangeL, contDiffOn_succ_iff_fderiv_of_isOpen, hasFTaylorSeriesUpToOn_succ_iff_right, SchwartzMap.smulRightCLM_apply_apply, MeasureTheory.setToFun_smul_left, LinearMap.IsSymmetric.toSelfAdjoint_apply, ContMDiffOn.clm_comp, ContDiffWithinAt.clm_comp, IsContinuousRiemannianBundle.exists_continuous, contMDiffOn_continuousLinearMapCoordChange, ContDiff.smulRight, Real.fourier_fderiv, hasFTaylorSeriesUpTo_succ_nat_iff_right, HasFDerivWithinAt.norm_sq, MDifferentiableAt.clm_comp, VectorFourier.fderiv_fourierIntegral, hasFTaylorSeriesUpToOn_succ_nat_iff_right, Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, FormalMultilinearSeries.radius_unshift, hasStrictFDerivAt_norm_sq, SchwartzMap.fourier_evalCLM_eq, contDiffOn_infty_iff_fderiv_of_isOpen, SchwartzMap.evalCLM_apply_apply, contMDiffOn_symm_coordChangeL, contMDiffAt_hom_bundle, TestFunction.lineDerivCLM_eq_fderivCLM, ContDiffOn.clm_comp, ContMDiffAt.clm_precomp, MDifferentiable.clm_prodMap, HasFTaylorSeriesUpToOn.shift_of_succ, contDiffOn_fderiv_coord_change, MeasureTheory.L1.SimpleFunc.setToL1SCLM_smul_left, ContDiff.clm_comp, ContDiffWithinAt.fderivWithin', contDiffAt_succ_iff_hasFDerivAt, MDifferentiableOn.cle_arrowCongr, ContMDiffWithinAt.mfderivWithin, MDifferentiableAt.clm_precomp, iteratedFDeriv_succ_apply_right, mdifferentiableOn_continuousLinearMapCoordChange, ContDiffMapSupportedIn.fderivCLM_eq_of_scalars, contDiff_clm_apply_iff, contDiffOn_clm_apply, HasFDerivWithinAt.clm_comp, IsInvertible.contDiffAt_map_inverse, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem, TestFunction.fderivCLM_eq_of_scalars, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, Real.fourierIntegral_fderiv, MDifferentiableWithinAt.clm_comp, MDifferentiableOn.clm_comp, ContMDiffAt.clm_prodMap, SchwartzMap.tsupport_fderivCLM_subset, intervalIntegral_apply, AnalyticOnNhd.fderiv, iteratedFDeriv_succ_eq_comp_right, ContDiffOn.fderivWithin, Real.hasFDerivAt_fourierIntegral, FormalMultilinearSeries.radius_shift, mdifferentiableOn_coordChangeL, ContMDiffVectorBundle.contMDiffOn_coordChangeL, fderivWithin_clm_comp, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, ContMDiff.clm_postcomp, MDifferentiableAt.coordChangeL, ContDiffAt.clm_comp, MDifferentiableWithinAt.clm_postcomp, ContMDiff.clm_prodMap, TestFunction.fderivCLM_apply_of_gt, SchwartzMap.fderivCLM_fourier_eq, ContDiffAt.fderiv, MDifferentiableOn.clm_precomp, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, contDiffOn_succ_iff_fderivWithin, ContDiffMapSupportedIn.fderivLM_apply, ContDiffWithinAt.fderivWithin, ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap, ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap, ContDiffPointwiseHolderAt.fderiv, Real.fourierIntegral_continuousLinearMap_apply', hasFDerivAt_integral_of_dominated_of_fderiv_le, CPolynomialOn.fderiv, ContMDiffCovariantDerivativeOn.contMDiff, ContDiffWithinAt.smulRight, ContMDiffWithinAt.coordChangeL, FormalMultilinearSeries.radius_le_radius_derivSeries, ContMDiffFiberwiseLinear.locality_aux₁, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, ContMDiffAt.mfderiv, VectorPrebundle.contMDiffOn_contMDiffCoordChange, mdifferentiableAt_coordChangeL, ContDiffMapSupportedIn.fderivCLM_apply_of_le, hasFDerivAt_integral_of_dominated_of_fderiv_le'', HasFiniteFPowerSeriesOnBall.fderiv', iteratedFDerivWithin_clm_apply_const_apply, ContMDiffWithinAt.clm_prodMap, ContDiffMapSupportedIn.fderivCLM_apply, TestFunction.fderivCLM_apply, SchwartzMap.fourier_fderivCLM_eq, ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap, MDifferentiable.clm_precomp, MDifferentiable.clm_comp, ContDiffMapSupportedIn.fderivLM_apply_of_le, ContMDiff.clm_comp, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, ContDiffMapSupportedIn.fderivLM_apply_of_gt, contMDiffOn_coordChangeL, ContMDiffWithinAt.clm_precomp, norm_iteratedFDerivWithin_fderivWithin, ContDiffOn.smulRight, ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap, ContMDiff.clm_precomp, ContMDiffOn.clm_prodMap, ContMDiffWithinAt.clm_comp, AnalyticAt.fderiv, iteratedFDeriv_clm_apply_const_apply, ContDiff.fderiv_right, contDiff_infty_iff_fderiv, HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn, exists_continuousLinearEquiv_fderiv_symm_eq, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, ContMDiffWithinAt.cle_arrowCongr, ContDiff.fderiv, exists_continuousLinearEquiv_fderivWithin_symm_eq, HasStrictFDerivAt.clm_comp, ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap, DoubleCentralizer.toProdHom_apply, VectorFourier.fourierIntegral_fderiv, MDifferentiableWithinAt.clm_prodMap, ContMDiffAt.clm_comp, ContDiffAt.smulRight, mdifferentiableWithinAt_hom_bundle, ContMDiffAt.cle_arrowCongr, HasFDerivAt.clm_comp, contMDiffWithinAt_hom_bundle, mem_contMDiffFiberwiseLinear_iff, fderiv_norm_sq_apply, norm_iteratedFDeriv_fderiv, fderiv_norm_sq, ContMDiff.cle_arrowCongr, contDiff_succ_iff_hasFDerivAt, HasCompactSupport.hasFDerivAt_convolution_left, ContMDiff.coordChangeL, ContDiffWithinAt.fderivWithin_right, contDiffWithinAt_succ_iff_hasFDerivWithinAt, hasFDerivAt_integral_of_dominated_loc_of_lip, HasFiniteFPowerSeriesOnBall.fderiv, norm_iteratedFDeriv_clm_apply_const
toNormedRing 📖	CompOp	5 math math: isometry_mul_flip, DoubleCentralizer.norm_def', CStarMatrix.norm_def', instCStarRingId, instNonnegSpectrumClassRealId

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz_of_isEmbedding 📖	mathematical	Topology.IsEmbedding 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	NNReal AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule funLike	—	LinearMap.antilipschitz_of_comap_nhds_le RingHomIsometric.ids Eq.ge Topology.IsInducing.nhds_eq_comap Topology.IsEmbedding.toIsInducing map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
norm_inl 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instTopologicalSpaceProd Prod.instAddCommMonoid NormedSpace.toModule Prod.instModule hasOpNorm Prod.seminormedAddCommGroup Prod.normedSpace inl Real Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap RingHomIsometric.ids
norm_inl_le_one 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instTopologicalSpaceProd Prod.instAddCommMonoid NormedSpace.toModule Prod.instModule hasOpNorm Prod.seminormedAddCommGroup Prod.normedSpace inl Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap_le
norm_inr 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instTopologicalSpaceProd Prod.instAddCommMonoid NormedSpace.toModule Prod.instModule hasOpNorm Prod.seminormedAddCommGroup Prod.normedSpace inr Real Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap RingHomIsometric.ids
norm_inr_le_one 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instTopologicalSpaceProd Prod.instAddCommMonoid NormedSpace.toModule Prod.instModule hasOpNorm Prod.seminormedAddCommGroup Prod.normedSpace inr Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap_le
norm_single 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.topologicalSpace Pi.addCommMonoid NormedSpace.toModule Pi.module hasOpNorm Pi.seminormedAddCommGroup Pi.normedSpace single Real Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap RingHomIsometric.ids
norm_single_le_one 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Pi.topologicalSpace Pi.addCommMonoid NormedSpace.toModule Pi.module hasOpNorm Pi.seminormedAddCommGroup Pi.normedSpace single Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap_le
norm_smulRightL 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 NormedSpace.toIsBoundedSMul hasOpNorm toSeminormedAddCommGroup RingHomIsometric.ids toNormedSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DFunLike.coe StrongDual NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Semiring.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing addCommGroup NormedRing.toRing NormedCommRing.toNormedRing topologicalAddGroup NormedField.toNormedSpace Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul smulCommClass continuousConstSMul funLike smulRightL	—	homothety_norm RingHomIsometric.ids smulCommClass_self EMetric.instNontrivialTopologyOfNontrivial SeminormedAddCommGroup.toIsTopologicalAddGroup IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalAddGroup.toContinuousAdd UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul topologicalAddGroup Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul smulCommClass continuousConstSMul norm_smulRight_apply
norm_smulRightL_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule topologicalSpace NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Semiring.toModule SeminormedAddCommGroup.toIsTopologicalAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul addCommGroup NormedRing.toRing NormedCommRing.toNormedRing topologicalAddGroup toSeminormedAddCommGroup RingHomIsometric.ids NormedField.toNormedSpace Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul smulCommClass continuousConstSMul hasOpNorm toNormedSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid smulRightL Real.instOne	—	LinearMap.mkContinuous₂_norm_le zero_le_one Real.instZeroLEOneClass
opNorm_comp_linearIsometryEquiv 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule hasOpNorm comp LinearIsometry.toContinuousLinearMap LinearIsometryEquiv.toLinearIsometry	—	subsingleton_or_nontrivial opNorm_subsingleton Equiv.subsingleton le_antisymm LinearIsometry.norm_toContinuousLinearMap mul_one opNorm_comp_le ext LinearIsometryEquiv.apply_symm_apply Function.Surjective.nontrivial LinearIsometryEquiv.surjective
opNorm_zero_iff 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule hasOpNorm Real Real.instZero zero	—	ext norm_le_zero_iff le_opNorm MulZeroClass.zero_mul opNorm_zero

LinearIsometry

Definitions

Name	Category	Theorems
inl 📖	CompOp	1 math math: inl_apply
inr 📖	CompOp	1 math math: inr_apply
postcomp 📖	CompOp	—
single 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enorm_toContinuousLinearMap 📖	mathematical	—	ENorm.enorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousENorm.toENorm SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm toContinuousLinearMap ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	nnnorm_toContinuousLinearMap
inl_apply 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Prod.seminormedAddCommGroup NormedSpace.toModule Prod.instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instFunLike inl NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
inr_apply 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Prod.seminormedAddCommGroup NormedSpace.toModule Prod.instModule AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup instFunLike inr NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
nnnorm_toContinuousLinearMap 📖	mathematical	—	NNNorm.nnnorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup toContinuousLinearMap NNReal NNReal.instOne	—	norm_toContinuousLinearMap
norm_toContinuousLinearMap 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.hasOpNorm toContinuousLinearMap Real Real.instOne	—	ContinuousLinearMap.homothety_norm EMetric.instNontrivialTopologyOfNontrivial norm_map one_mul
norm_toContinuousLinearMap_comp 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.hasOpNorm ContinuousLinearMap.comp toContinuousLinearMap	—	ContinuousLinearMap.opNorm_ext norm_map

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz_of_comap_nhds_le 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.comap DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	NNReal AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike	—	Filter.HasBasis.le_basis_iff Filter.HasBasis.comap Metric.nhds_basis_ball one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing CanLift.prf NNReal.canLift LT.lt.le NormedField.exists_one_lt_norm AddMonoidHomClass.antilipschitz_of_bound DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass Eq.trans_le norm_zero mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg norm_nonneg Specializes.eq T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace specializes_iff_pure LE.le.trans Filter.Tendsto.le_comap Filter.Tendsto.mono_right Filter.tendsto_pure_pure pure_le_nhds norm_pos_iff LT.lt.trans rescale_to_shell_zpow RingHomIsometric.norm_map norm_inv norm_smul NormedSpace.toNormSMulClass inv_smul_smul₀ zpow_ne_zero mul_le_mul_of_nonneg_left RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass SemilinearMapClass.toMulActionSemiHomClass inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_one
bound_of_ball_bound 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Norm.norm NormedAddCommGroup.toNorm DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike Real.instMul	—	NontriviallyNormedField.non_trivial bound_of_shell RingHomIsometric.ids mem_ball_zero_iff le_mul_of_one_le_right IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_trans norm_nonneg dist_self one_le_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw
bound_of_shell 📖	mathematical	Real Real.instLT Real.instZero Real.instOne Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Real.instLE NormedAddCommGroup.toNorm DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike Real.instMul	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike Real.instMul	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass norm_zero MulZeroClass.mul_zero instReflLe SemilinearMapClass.bound_of_shell_semi_normed norm_ne_zero_iff

NormedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equicontinuous_TFAE 📖	mathematical	—	List.TFAE EquicontinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup toModule DFunLike.coe ContinuousLinearMap.funLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Equicontinuous UniformEquicontinuous Real Real.instLE Real.instZero BddAbove Set.range Norm.norm ContinuousLinearMap.hasOpNorm ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder ENNReal.ofNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup Top.top instTopENNReal	—	uniformEquicontinuous_of_equicontinuousAt_zero SeminormedAddCommGroup.to_isUniformAddGroup DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass UniformEquicontinuous.equicontinuous exists_ge_and_iff_exists forall₂_imp le_trans' mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg ContinuousLinearMap.opNorm_le_iff bddAbove_iff_exists_ge ENNReal.iSup_coe_lt_top NNReal.bddAbove_coe Set.range_comp WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm norm_withSeminorms IsBoundedSMul.continuousSMul toIsBoundedSMul Seminorm.bound_of_continuous_normedSpace LE.le.trans IsScalarTower.left Continuous.const_smul SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal WithSeminorms.continuous_seminorm Real.le_coe_toNNReal List.tfae_of_cycle

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_subtypeL 📖	mathematical	—	Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.hasOpNorm seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing normedSpace Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction subtypeL Real Real.instOne	—	LinearIsometry.norm_toContinuousLinearMap IsScalarTower.left RingHomIsometric.ids

(root)

Definitions

Name	Category	Theorems
IsCoercive 📖	MathDef	—

---

← Back to Index