Commit 2024-02-27 00:53 7aeba51a

View on Github →

chore(Analysis/NormedSpace): split up OperatorNorm.lean (#10990) Split the 2300-line behemoth OperatorNorm.lean into 8 smaller files, of which the largest is 600 lines.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

Modified Mathlib/Analysis/Complex/OperatorNorm.lean

Modified Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean

Modified Mathlib/Analysis/NormedSpace/Banach.lean

Modified Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean

Modified Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

Modified Mathlib/Analysis/NormedSpace/Completion.lean

Modified Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

Modified Mathlib/Analysis/NormedSpace/Extend.lean

Modified Mathlib/Analysis/NormedSpace/FiniteDimension.lean

Modified Mathlib/Analysis/NormedSpace/IsROrC.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Deleted Mathlib/Analysis/NormedSpace/OperatorNorm.lean

deleted theorem Continuous.clm_comp_const

deleted theorem Continuous.const_clm_comp

deleted theorem Continuous.prod_mapL

deleted theorem Continuous.prod_map_equivL

deleted theorem ContinuousLinearEquiv.coord_norm

deleted theorem ContinuousLinearEquiv.isBigO_comp

deleted theorem ContinuousLinearEquiv.isBigO_comp_rev

deleted theorem ContinuousLinearEquiv.isBigO_sub

deleted theorem ContinuousLinearEquiv.isBigO_sub_rev

deleted theorem ContinuousLinearEquiv.nnnorm_symm_pos

deleted theorem ContinuousLinearEquiv.norm_pos

deleted theorem ContinuousLinearEquiv.norm_symm_pos

deleted theorem ContinuousLinearEquiv.one_le_norm_mul_norm_symm

deleted theorem ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos

deleted theorem ContinuousLinearEquiv.subsingleton_or_norm_symm_pos

deleted theorem ContinuousLinearMap.antilipschitz_of_embedding

deleted def ContinuousLinearMap.apply'

deleted def ContinuousLinearMap.apply

deleted theorem ContinuousLinearMap.apply_apply'

deleted theorem ContinuousLinearMap.apply_apply

deleted def ContinuousLinearMap.bilinearComp

deleted theorem ContinuousLinearMap.bilinearComp_apply

deleted theorem ContinuousLinearMap.bound

deleted theorem ContinuousLinearMap.bounds_bddBelow

deleted theorem ContinuousLinearMap.bounds_nonempty

deleted theorem ContinuousLinearMap.coe_deriv₂

deleted theorem ContinuousLinearMap.coe_flipₗᵢ'

deleted theorem ContinuousLinearMap.coe_flipₗᵢ

deleted theorem ContinuousLinearMap.coe_mulₗᵢ

deleted theorem ContinuousLinearMap.coe_restrictScalarsIsometry

deleted theorem ContinuousLinearMap.coe_restrictScalarsL

deleted theorem ContinuousLinearMap.coe_restrict_scalarsL'

deleted def ContinuousLinearMap.compL

deleted theorem ContinuousLinearMap.compL_apply

deleted def ContinuousLinearMap.compSL

deleted theorem ContinuousLinearMap.compSL_apply

deleted def ContinuousLinearMap.deriv₂

deleted theorem ContinuousLinearMap.dist_le_opNorm

deleted theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm

deleted theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNorm

deleted theorem ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm

deleted theorem ContinuousLinearMap.exists_mul_lt_of_lt_opNorm

deleted def ContinuousLinearMap.extend

deleted theorem ContinuousLinearMap.extend_eq

deleted theorem ContinuousLinearMap.extend_unique

deleted theorem ContinuousLinearMap.extend_zero

deleted def ContinuousLinearMap.flip

deleted theorem ContinuousLinearMap.flip_add

deleted theorem ContinuousLinearMap.flip_apply

deleted theorem ContinuousLinearMap.flip_flip

deleted theorem ContinuousLinearMap.flip_smul

deleted def ContinuousLinearMap.flipₗᵢ'

deleted theorem ContinuousLinearMap.flipₗᵢ'_symm

deleted def ContinuousLinearMap.flipₗᵢ

deleted theorem ContinuousLinearMap.flipₗᵢ_symm

deleted theorem ContinuousLinearMap.homothety_norm

deleted theorem ContinuousLinearMap.isBigOWith_comp

deleted theorem ContinuousLinearMap.isBigOWith_id

deleted theorem ContinuousLinearMap.isBigOWith_sub

deleted theorem ContinuousLinearMap.isBigO_comp

deleted theorem ContinuousLinearMap.isBigO_id

deleted theorem ContinuousLinearMap.isBigO_sub

deleted theorem ContinuousLinearMap.isClosed_image_coe_closedBall

deleted theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed

deleted theorem ContinuousLinearMap.isCompact_closure_image_coe_of_bounded

deleted theorem ContinuousLinearMap.isCompact_image_coe_closedBall

deleted theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image

deleted theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed

deleted theorem ContinuousLinearMap.isLeast_opNNNorm

deleted theorem ContinuousLinearMap.isLeast_opNorm

deleted theorem ContinuousLinearMap.is_weak_closed_closedBall

deleted theorem ContinuousLinearMap.isometry_mul

deleted theorem ContinuousLinearMap.le_of_opNorm_le

deleted theorem ContinuousLinearMap.le_of_opNorm_le_of_le

deleted theorem ContinuousLinearMap.le_of_opNorm₂_le_of_le

deleted theorem ContinuousLinearMap.le_opNNNorm

deleted theorem ContinuousLinearMap.le_opNorm

deleted theorem ContinuousLinearMap.le_opNorm_of_le

deleted theorem ContinuousLinearMap.le_opNorm₂

deleted theorem ContinuousLinearMap.lipschitz

deleted theorem ContinuousLinearMap.lipschitz_apply

deleted def ContinuousLinearMap.lsmul

deleted theorem ContinuousLinearMap.lsmul_apply

deleted theorem ContinuousLinearMap.map_add_add

deleted def ContinuousLinearMap.mul

deleted def ContinuousLinearMap.mulLeftRight

deleted theorem ContinuousLinearMap.mulLeftRight_apply

deleted theorem ContinuousLinearMap.mul_apply'

deleted def ContinuousLinearMap.mulₗᵢ

deleted theorem ContinuousLinearMap.nndist_le_opNNNorm

deleted theorem ContinuousLinearMap.nnnorm_def

deleted theorem ContinuousLinearMap.nnnorm_id

deleted theorem ContinuousLinearMap.nnnorm_smulRight_apply

deleted theorem ContinuousLinearMap.norm_compL_le

deleted theorem ContinuousLinearMap.norm_compSL_le

deleted theorem ContinuousLinearMap.norm_def

deleted theorem ContinuousLinearMap.norm_id

deleted theorem ContinuousLinearMap.norm_id_le

deleted theorem ContinuousLinearMap.norm_id_of_nontrivial_seminorm

deleted theorem ContinuousLinearMap.norm_precompL_le

deleted theorem ContinuousLinearMap.norm_precompR_le

deleted theorem ContinuousLinearMap.norm_restrictScalars

deleted theorem ContinuousLinearMap.norm_smulRightL

deleted theorem ContinuousLinearMap.norm_smulRightL_apply

deleted theorem ContinuousLinearMap.norm_smulRight_apply

deleted theorem ContinuousLinearMap.norm_toSpanSingleton

deleted def ContinuousLinearMap.ofMemClosureImageCoeBounded

deleted def ContinuousLinearMap.ofTendstoOfBoundedRange

deleted theorem ContinuousLinearMap.opNNNorm_comp_le

deleted theorem ContinuousLinearMap.opNNNorm_eq_of_bounds

deleted theorem ContinuousLinearMap.opNNNorm_le_bound'

deleted theorem ContinuousLinearMap.opNNNorm_le_bound

deleted theorem ContinuousLinearMap.opNNNorm_le_iff

deleted theorem ContinuousLinearMap.opNNNorm_le_of_lipschitz

deleted theorem ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm

deleted theorem ContinuousLinearMap.opNNNorm_mul

deleted theorem ContinuousLinearMap.opNNNorm_mul_apply

deleted theorem ContinuousLinearMap.opNNNorm_prod

deleted def ContinuousLinearMap.opNorm

deleted theorem ContinuousLinearMap.opNorm_add_le

deleted theorem ContinuousLinearMap.opNorm_comp_le

deleted theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv

deleted theorem ContinuousLinearMap.opNorm_eq_of_bounds

deleted theorem ContinuousLinearMap.opNorm_ext

deleted theorem ContinuousLinearMap.opNorm_extend_le

deleted theorem ContinuousLinearMap.opNorm_flip

deleted theorem ContinuousLinearMap.opNorm_le_bound'

deleted theorem ContinuousLinearMap.opNorm_le_bound

deleted theorem ContinuousLinearMap.opNorm_le_bound₂

deleted theorem ContinuousLinearMap.opNorm_le_iff

deleted theorem ContinuousLinearMap.opNorm_le_of_ball

deleted theorem ContinuousLinearMap.opNorm_le_of_lipschitz

deleted theorem ContinuousLinearMap.opNorm_le_of_nhds_zero

deleted theorem ContinuousLinearMap.opNorm_le_of_shell'

deleted theorem ContinuousLinearMap.opNorm_le_of_shell

deleted theorem ContinuousLinearMap.opNorm_le_of_unit_norm

deleted theorem ContinuousLinearMap.opNorm_lsmul

deleted theorem ContinuousLinearMap.opNorm_lsmul_apply_le

deleted theorem ContinuousLinearMap.opNorm_lsmul_le

deleted theorem ContinuousLinearMap.opNorm_mul

deleted theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le

deleted theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_le

deleted theorem ContinuousLinearMap.opNorm_mulLeftRight_le

deleted theorem ContinuousLinearMap.opNorm_mul_apply

deleted theorem ContinuousLinearMap.opNorm_mul_apply_le

deleted theorem ContinuousLinearMap.opNorm_mul_le

deleted theorem ContinuousLinearMap.opNorm_neg

deleted theorem ContinuousLinearMap.opNorm_nonneg

deleted theorem ContinuousLinearMap.opNorm_prod

deleted theorem ContinuousLinearMap.opNorm_smul_le

deleted theorem ContinuousLinearMap.opNorm_subsingleton

deleted theorem ContinuousLinearMap.opNorm_zero

deleted theorem ContinuousLinearMap.opNorm_zero_iff

deleted def ContinuousLinearMap.precompL

deleted def ContinuousLinearMap.precompR

deleted def ContinuousLinearMap.prodMapL

deleted theorem ContinuousLinearMap.prodMapL_apply

deleted def ContinuousLinearMap.prodₗᵢ

deleted theorem ContinuousLinearMap.ratio_le_opNorm

deleted def ContinuousLinearMap.restrictScalarsIsometry

deleted theorem ContinuousLinearMap.restrictScalarsIsometry_toLinearMap

deleted def ContinuousLinearMap.restrictScalarsL

deleted def ContinuousLinearMap.ring_lmap_equiv_self

deleted def ContinuousLinearMap.ring_lmap_equiv_selfₗ

deleted theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_nnnorm

deleted theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_norm

deleted theorem ContinuousLinearMap.sSup_unit_ball_eq_nnnorm

deleted theorem ContinuousLinearMap.sSup_unit_ball_eq_norm

deleted def ContinuousLinearMap.smulRightL

deleted theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq

deleted theorem ContinuousLinearMap.unit_le_opNorm

deleted theorem ContinuousOn.prod_mapL

deleted theorem ContinuousOn.prod_map_equivL

deleted def IsCoercive

deleted theorem LinearIsometry.coe_toSpanSingleton

deleted theorem LinearIsometry.norm_toContinuousLinearMap

deleted theorem LinearIsometry.norm_toContinuousLinearMap_comp

deleted theorem LinearIsometry.norm_toContinuousLinearMap_le

deleted def LinearIsometry.toSpanSingleton

deleted theorem LinearIsometry.toSpanSingleton_apply

deleted theorem LinearMap.antilipschitz_of_comap_nhds_le

deleted theorem LinearMap.bound_of_ball_bound

deleted theorem LinearMap.bound_of_shell

deleted def LinearMap.mkContinuousOfExistsBound₂

deleted theorem LinearMap.mkContinuous_norm_le'

deleted theorem LinearMap.mkContinuous_norm_le

deleted def LinearMap.mkContinuous₂

deleted theorem LinearMap.mkContinuous₂_apply

deleted theorem LinearMap.mkContinuous₂_norm_le'

deleted theorem LinearMap.mkContinuous₂_norm_le

deleted theorem LinearMap.norm_mkContinuous₂_aux

deleted def NonUnitalAlgHom.Lmul

deleted theorem NonUnitalAlgHom.coe_Lmul

deleted theorem SemilinearMapClass.bound_of_continuous

deleted theorem SemilinearMapClass.bound_of_shell_semi_normed

deleted theorem Submodule.norm_subtypeL

deleted theorem Submodule.norm_subtypeL_le

deleted theorem norm_image_of_norm_zero

Created Mathlib/Analysis/NormedSpace/OperatorNorm/Asymptotics.lean

added theorem ContinuousLinearEquiv.isBigO_comp

added theorem ContinuousLinearEquiv.isBigO_comp_rev

added theorem ContinuousLinearEquiv.isBigO_sub

added theorem ContinuousLinearEquiv.isBigO_sub_rev

added theorem ContinuousLinearMap.isBigOWith_comp

added theorem ContinuousLinearMap.isBigOWith_id

added theorem ContinuousLinearMap.isBigOWith_sub

added theorem ContinuousLinearMap.isBigO_comp

added theorem ContinuousLinearMap.isBigO_id

added theorem ContinuousLinearMap.isBigO_sub

Created Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean

added theorem ContinuousLinearMap.bound

added theorem ContinuousLinearMap.bounds_bddBelow

added theorem ContinuousLinearMap.bounds_nonempty

added theorem ContinuousLinearMap.coe_restrictScalarsIsometry

added theorem ContinuousLinearMap.coe_restrictScalarsL

added theorem ContinuousLinearMap.coe_restrict_scalarsL'

added theorem ContinuousLinearMap.dist_le_opNorm

added theorem ContinuousLinearMap.isLeast_opNorm

added theorem ContinuousLinearMap.le_of_opNorm_le

added theorem ContinuousLinearMap.le_of_opNorm_le_of_le

added theorem ContinuousLinearMap.le_opNorm

added theorem ContinuousLinearMap.le_opNorm_of_le

added theorem ContinuousLinearMap.norm_def

added theorem ContinuousLinearMap.norm_id_le

added theorem ContinuousLinearMap.norm_id_of_nontrivial_seminorm

added theorem ContinuousLinearMap.norm_restrictScalars

added def ContinuousLinearMap.opNorm

added theorem ContinuousLinearMap.opNorm_add_le

added theorem ContinuousLinearMap.opNorm_comp_le

added theorem ContinuousLinearMap.opNorm_eq_of_bounds

added theorem ContinuousLinearMap.opNorm_le_bound'

added theorem ContinuousLinearMap.opNorm_le_bound

added theorem ContinuousLinearMap.opNorm_le_iff

added theorem ContinuousLinearMap.opNorm_le_of_ball

added theorem ContinuousLinearMap.opNorm_le_of_lipschitz

added theorem ContinuousLinearMap.opNorm_le_of_nhds_zero

added theorem ContinuousLinearMap.opNorm_le_of_shell'

added theorem ContinuousLinearMap.opNorm_le_of_shell

added theorem ContinuousLinearMap.opNorm_le_of_unit_norm

added theorem ContinuousLinearMap.opNorm_neg

added theorem ContinuousLinearMap.opNorm_nonneg

added theorem ContinuousLinearMap.opNorm_smul_le

added theorem ContinuousLinearMap.opNorm_subsingleton

added theorem ContinuousLinearMap.opNorm_zero

added theorem ContinuousLinearMap.ratio_le_opNorm

added def ContinuousLinearMap.restrictScalarsIsometry

added theorem ContinuousLinearMap.restrictScalarsIsometry_toLinearMap

added def ContinuousLinearMap.restrictScalarsL

added theorem ContinuousLinearMap.unit_le_opNorm

added theorem LinearIsometry.coe_toSpanSingleton

added theorem LinearIsometry.norm_toContinuousLinearMap_le

added def LinearIsometry.toSpanSingleton

added theorem LinearIsometry.toSpanSingleton_apply

added theorem LinearMap.mkContinuous_norm_le'

added theorem LinearMap.mkContinuous_norm_le

added theorem SemilinearMapClass.bound_of_continuous

added theorem SemilinearMapClass.bound_of_shell_semi_normed

added theorem Submodule.norm_subtypeL_le

added theorem norm_image_of_norm_zero

Created Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

added theorem Continuous.clm_comp_const

added theorem Continuous.const_clm_comp

added def ContinuousLinearMap.apply'

added def ContinuousLinearMap.apply

added theorem ContinuousLinearMap.apply_apply'

added theorem ContinuousLinearMap.apply_apply

added def ContinuousLinearMap.bilinearComp

added theorem ContinuousLinearMap.bilinearComp_apply

added theorem ContinuousLinearMap.coe_deriv₂

added theorem ContinuousLinearMap.coe_flipₗᵢ'

added theorem ContinuousLinearMap.coe_flipₗᵢ

added def ContinuousLinearMap.compL

added theorem ContinuousLinearMap.compL_apply

added def ContinuousLinearMap.compSL

added theorem ContinuousLinearMap.compSL_apply

added def ContinuousLinearMap.deriv₂

added def ContinuousLinearMap.flip

added theorem ContinuousLinearMap.flip_add

added theorem ContinuousLinearMap.flip_apply

added theorem ContinuousLinearMap.flip_flip

added theorem ContinuousLinearMap.flip_smul

added def ContinuousLinearMap.flipₗᵢ'

added theorem ContinuousLinearMap.flipₗᵢ'_symm

added def ContinuousLinearMap.flipₗᵢ

added theorem ContinuousLinearMap.flipₗᵢ_symm

added theorem ContinuousLinearMap.le_of_opNorm₂_le_of_le

added theorem ContinuousLinearMap.le_opNorm₂

added theorem ContinuousLinearMap.map_add_add

added theorem ContinuousLinearMap.norm_compL_le

added theorem ContinuousLinearMap.norm_compSL_le

added theorem ContinuousLinearMap.norm_precompL_le

added theorem ContinuousLinearMap.norm_precompR_le

added theorem ContinuousLinearMap.opNorm_ext

added theorem ContinuousLinearMap.opNorm_flip

added theorem ContinuousLinearMap.opNorm_le_bound₂

added def ContinuousLinearMap.precompL

added def ContinuousLinearMap.precompR

added def LinearMap.mkContinuousOfExistsBound₂

added def LinearMap.mkContinuous₂

added theorem LinearMap.mkContinuous₂_apply

added theorem LinearMap.mkContinuous₂_norm_le'

added theorem LinearMap.mkContinuous₂_norm_le

added theorem LinearMap.norm_mkContinuous₂_aux

Created Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean

added def ContinuousLinearMap.extend

added theorem ContinuousLinearMap.extend_eq

added theorem ContinuousLinearMap.extend_unique

added theorem ContinuousLinearMap.extend_zero

added theorem ContinuousLinearMap.isClosed_image_coe_closedBall

added theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed

added theorem ContinuousLinearMap.isCompact_closure_image_coe_of_bounded

added theorem ContinuousLinearMap.isCompact_image_coe_closedBall

added theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image

added theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed

added theorem ContinuousLinearMap.is_weak_closed_closedBall

added def ContinuousLinearMap.ofMemClosureImageCoeBounded

added def ContinuousLinearMap.ofTendstoOfBoundedRange

added theorem ContinuousLinearMap.opNorm_extend_le

added theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq

Created Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean

added theorem ContinuousLinearMap.coe_mulₗᵢ

added theorem ContinuousLinearMap.isometry_mul

added def ContinuousLinearMap.lsmul

added theorem ContinuousLinearMap.lsmul_apply

added def ContinuousLinearMap.mul

added def ContinuousLinearMap.mulLeftRight

added theorem ContinuousLinearMap.mulLeftRight_apply

added theorem ContinuousLinearMap.mul_apply'

added def ContinuousLinearMap.mulₗᵢ

added theorem ContinuousLinearMap.norm_toSpanSingleton

added theorem ContinuousLinearMap.opNNNorm_mul

added theorem ContinuousLinearMap.opNNNorm_mul_apply

added theorem ContinuousLinearMap.opNorm_lsmul

added theorem ContinuousLinearMap.opNorm_lsmul_apply_le

added theorem ContinuousLinearMap.opNorm_lsmul_le

added theorem ContinuousLinearMap.opNorm_mul

added theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le

added theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_le

added theorem ContinuousLinearMap.opNorm_mulLeftRight_le

added theorem ContinuousLinearMap.opNorm_mul_apply

added theorem ContinuousLinearMap.opNorm_mul_apply_le

added theorem ContinuousLinearMap.opNorm_mul_le

added def ContinuousLinearMap.ring_lmap_equiv_self

added def ContinuousLinearMap.ring_lmap_equiv_selfₗ

added def NonUnitalAlgHom.Lmul

added theorem NonUnitalAlgHom.coe_Lmul

Created Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

added theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm

added theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNorm

added theorem ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm

added theorem ContinuousLinearMap.exists_mul_lt_of_lt_opNorm

added theorem ContinuousLinearMap.isLeast_opNNNorm

added theorem ContinuousLinearMap.le_opNNNorm

added theorem ContinuousLinearMap.lipschitz

added theorem ContinuousLinearMap.lipschitz_apply

added theorem ContinuousLinearMap.nndist_le_opNNNorm

added theorem ContinuousLinearMap.nnnorm_def

added theorem ContinuousLinearMap.opNNNorm_comp_le

added theorem ContinuousLinearMap.opNNNorm_eq_of_bounds

added theorem ContinuousLinearMap.opNNNorm_le_bound'

added theorem ContinuousLinearMap.opNNNorm_le_bound

added theorem ContinuousLinearMap.opNNNorm_le_iff

added theorem ContinuousLinearMap.opNNNorm_le_of_lipschitz

added theorem ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm

added theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_nnnorm

added theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_norm

added theorem ContinuousLinearMap.sSup_unit_ball_eq_nnnorm

added theorem ContinuousLinearMap.sSup_unit_ball_eq_norm

Created Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean

added theorem ContinuousLinearEquiv.coord_norm

added theorem ContinuousLinearEquiv.nnnorm_symm_pos

added theorem ContinuousLinearEquiv.norm_pos

added theorem ContinuousLinearEquiv.norm_symm_pos

added theorem ContinuousLinearEquiv.one_le_norm_mul_norm_symm

added theorem ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos

added theorem ContinuousLinearEquiv.subsingleton_or_norm_symm_pos

added theorem ContinuousLinearMap.antilipschitz_of_embedding

added theorem ContinuousLinearMap.homothety_norm

added theorem ContinuousLinearMap.nnnorm_id

added theorem ContinuousLinearMap.nnnorm_smulRight_apply

added theorem ContinuousLinearMap.norm_id

added theorem ContinuousLinearMap.norm_smulRightL

added theorem ContinuousLinearMap.norm_smulRightL_apply

added theorem ContinuousLinearMap.norm_smulRight_apply

added theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv

added theorem ContinuousLinearMap.opNorm_zero_iff

added def ContinuousLinearMap.smulRightL

added def IsCoercive

added theorem LinearIsometry.norm_toContinuousLinearMap

added theorem LinearIsometry.norm_toContinuousLinearMap_comp

added theorem LinearMap.antilipschitz_of_comap_nhds_le

added theorem LinearMap.bound_of_ball_bound

added theorem LinearMap.bound_of_shell

added theorem Submodule.norm_subtypeL

Created Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean

added theorem Continuous.prod_mapL

added theorem Continuous.prod_map_equivL

added theorem ContinuousLinearMap.opNNNorm_prod

added theorem ContinuousLinearMap.opNorm_prod

added def ContinuousLinearMap.prodMapL

added theorem ContinuousLinearMap.prodMapL_apply

added def ContinuousLinearMap.prodₗᵢ

added theorem ContinuousOn.prod_mapL

added theorem ContinuousOn.prod_map_equivL

Modified Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

Modified Mathlib/Analysis/NormedSpace/Unitization.lean

Modified Mathlib/Analysis/NormedSpace/WeakDual.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/ContinuousLinearMap.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Modified Mathlib/Topology/ContinuousFunction/Compact.lean

Modified Mathlib/Topology/VectorBundle/Constructions.lean

Modified Mathlib/Topology/VectorBundle/Hom.lean