Constructions

📁 Source: Mathlib/Analysis/Normed/Group/Constructions.lean

Statistics

Metric	Count
Definitions normedAddCommGroup, normedAddGroup, seminormedAddGroup, seminormedCommGroup, toNNNorm, toNorm, instNormedAddCommGroup, instNormedAddGroup, instSeminormedAddCommGroup, instSeminormedAddGroup, normedCommGroup, normedGroup, seminormedAddCommGroup, seminormedGroup, toNNNorm, toNorm, normedAddCommGroup, normedAddGroup, normedCommGroup, normedGroup, seminormedAddCommGroup, seminormedAddGroup, seminormedCommGroup, seminormedGroup, toNNNorm, toNorm, normedAddCommGroup, normedAddCommGroup, normedAddGroup, normedCommGroup, normedGroup, seminormedAddCommGroup, seminormedAddGroup, seminormedCommGroup, seminormedGroup, normedAddCommGroup, normedAddGroup, normedCommGroup, normedGroup, seminormedAddCommGroup, seminormedAddGroup, seminormedCommGroup, seminormedGroup, toNorm, nnnorm, norm, normedAddCommGroup, normedAddGroup, normedCommGroup, normedGroup, seminormedAddCommGroup, seminormedAddGroup, seminormedCommGroup, seminormedGroup	54
Theorems nnnorm_op, nnnorm_unop, norm_op, norm_unop, norm_eq_zero, enorm_single, nnnorm_def, nnnorm_def', nnnorm_single, norm_def, norm_def', norm_single, sum_nnnorm_apply_le_nnnorm, sum_nnnorm_apply_le_nnnorm', sum_norm_apply_le_norm, sum_norm_apply_le_norm', nnnorm_def, nnnorm_def', nnnorm_mk, nnnorm_mk', norm_def, norm_mk, nnnorm_def, nnnorm_down, nnnorm_up, norm_def, norm_down, norm_up, nnnorm_le_pi_nnnorm, nnnorm_le_pi_nnnorm', nnnorm_ofAdd, nnnorm_ofDual, nnnorm_ofMul, nnnorm_toAdd, nnnorm_toDual, nnnorm_toMul, norm_fst_le, norm_le_pi_norm, norm_le_pi_norm', norm_ofAdd, norm_ofDual, norm_ofMul, norm_prod_le_iff, norm_snd_le, norm_toAdd, norm_toDual, norm_toMul, pi_nnnorm_const, pi_nnnorm_const', pi_nnnorm_const_le, pi_nnnorm_const_le', pi_nnnorm_le_iff, pi_nnnorm_le_iff', pi_nnnorm_lt_iff, pi_nnnorm_lt_iff', pi_norm_const, pi_norm_const', pi_norm_const_le, pi_norm_const_le', pi_norm_le_iff_of_nonempty, pi_norm_le_iff_of_nonempty', pi_norm_le_iff_of_nonneg, pi_norm_le_iff_of_nonneg', pi_norm_lt_iff, pi_norm_lt_iff'	65
Total	119

Additive

Definitions

Name	Category	Theorems
normedAddCommGroup 📖	CompOp	—
normedAddGroup 📖	CompOp	—
seminormedAddGroup 📖	CompOp	—
seminormedCommGroup 📖	CompOp	—
toNNNorm 📖	CompOp	2 math math: nnnorm_toMul, nnnorm_ofMul
toNorm 📖	CompOp	2 math math: norm_ofMul, norm_toMul

MulOpposite

Definitions

Name	Category	Theorems
instNormedAddCommGroup 📖	CompOp	1 math math: OrthonormalBasis.toBasis_mulOpposite
instNormedAddGroup 📖	CompOp	—
instSeminormedAddCommGroup 📖	CompOp	6 math math: normOneClass, Module.Basis.mulOpposite_is_orthonormal_iff, toLinearEquiv_opLinearIsometryEquiv, opLinearIsometryEquiv_symm_apply, opLinearIsometryEquiv_apply, toContinuousLinearEquiv_opLinearIsometryEquiv
instSeminormedAddGroup 📖	CompOp	5 math math: DoubleCentralizer.nnnorm_def', nnnorm_unop, norm_unop, nnnorm_op, norm_op

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_op 📖	mathematical	—	NNNorm.nnnorm MulOpposite SeminormedAddGroup.toNNNorm instSeminormedAddGroup op	—	—
nnnorm_unop 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm unop MulOpposite instSeminormedAddGroup	—	—
norm_op 📖	mathematical	—	Norm.norm MulOpposite SeminormedAddGroup.toNorm instSeminormedAddGroup op	—	—
norm_unop 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm unop MulOpposite instSeminormedAddGroup	—	—

Multiplicative

Definitions

Name	Category	Theorems
normedCommGroup 📖	CompOp	—
normedGroup 📖	CompOp	—
seminormedAddCommGroup 📖	CompOp	—
seminormedGroup 📖	CompOp	—
toNNNorm 📖	CompOp	2 math math: nnnorm_ofAdd, nnnorm_toAdd
toNorm 📖	CompOp	2 math math: norm_ofAdd, norm_toAdd

OrderDual

Definitions

Name	Category	Theorems
normedAddCommGroup 📖	CompOp	1 math math: instHasSolidNorm
normedAddGroup 📖	CompOp	—
normedCommGroup 📖	CompOp	—
normedGroup 📖	CompOp	—
seminormedAddCommGroup 📖	CompOp	—
seminormedAddGroup 📖	CompOp	—
seminormedCommGroup 📖	CompOp	—
seminormedGroup 📖	CompOp	—
toNNNorm 📖	CompOp	2 math math: nnnorm_toDual, nnnorm_ofDual
toNorm 📖	CompOp	2 math math: norm_ofDual, norm_toDual

PUnit

Definitions

Name	Category	Theorems
normedAddCommGroup 📖	CompOp	6 math math: Manifold.IsImmersionAtOfComplement.ofOpen, norm_eq_zero, Manifold.IsImmersionOfComplement.ofOpen, Manifold.IsImmersionAtOfComplement.of_opens, Manifold.IsImmersionOfComplement.id, Manifold.IsImmersionOfComplement.of_opens

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_eq_zero 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm normedAddCommGroup Real Real.instZero	—	—

Pi

Definitions

Name	Category	Theorems
normedAddCommGroup 📖	CompOp	114 math math: NumberField.mixedEmbedding.fundamentalDomain_integerLattice, MeasureTheory.eval_integral, PiLp.contDiff_toLp, ContinuousMultilinearMap.cpolynomialOn, ZSpan.volume_real_fundamentalDomain, ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap, ContinuousMultilinearMap.analyticAt_uncurry_of_linear, FormalMultilinearSeries.radius_pi_eq_iInf, ZLattice.covolume_eq_det_inv, hasFPowerSeriesOnBall_pi_iff, ContinuousMultilinearMap.changeOrigin_toFormalMultilinearSeries, analyticWithinAt_pi_iff, ContinuousMultilinearMap.contDiffAt, Module.Basis.parallelepiped_basisFun, ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, analyticOnNhd_pi_iff, contDiffAt_pi', ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, contDiff_apply, ZLattice.covolume.tendsto_card_div_pow, NumberField.Units.instZLattice_unitLattice, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, ZLattice.covolume_div_covolume_eq_relIndex, contMDiffWithinAt_pi_space, contDiff_update, ZSpan.volume_fundamentalDomain, hasFTaylorSeriesUpToOn_pi', ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv, contMDiffOn_pi_space, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, AnalyticOn.pi, ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall, ContinuousMultilinearMap.analyticAt, NumberField.mixedEmbedding.covolume_idealLattice, ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear, contDiff_pi', HasFPowerSeriesWithinAt.pi, ContinuousMultilinearMap.contDiff, NumberField.Units.regOfFamily_of_isMaxRank, ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, contDiff_apply_apply, ContinuousMultilinearMap.iteratedFDeriv_eq, ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, AnalyticWithinAt.pi, contDiffAt_apply, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ContinuousMultilinearMap.cpolynomialAt, norm_single, ProbabilityTheory.iIndepFun_iff_charFunDual_pi, NumberField.mixedEmbedding.covolume_integerLattice, ContinuousMultilinearMap.analyticOn_uncurry_of_linear, hasFPowerSeriesAt_pi_iff, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, PiLp.analyticOn_ofLp, ContinuousMultilinearMap.norm_iteratedFDeriv_le, ZLattice.volume_image_eq_volume_div_covolume, PiLp.analyticOn_toLp, SmoothBumpCovering.embeddingPiTangent_injOn, hasFPowerSeriesWithinAt_pi_iff, MeasureTheory.charFunDual_eq_pi_iff, ContinuousMultilinearMap.changeOriginSeries_support, ZLattice.covolume.tendsto_card_le_div, HasFPowerSeriesOnBall.pi, analyticOn_pi_iff, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, ContinuousMultilinearMap.analyticOn, contDiff_single, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, SmoothBumpCovering.embeddingPiTangent_injective, PiLp.contDiff_ofLp, ContinuousMultilinearMap.analyticOnNhd, ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, hasFPowerSeriesWithinOnBall_pi_iff, ZSpan.fundamentalDomain_pi_basisFun, WithCStarModule.norm_equiv_le_norm_pi, contDiffWithinAt_pi, AnalyticOnNhd.pi, ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap, ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap, HasFPowerSeriesAt.pi, OrderedFinpartition.norm_compAlongOrderedFinpartition_sub_compAlongOrderedFinpartition_le, contDiffOn_pi, ContinuousMultilinearMap.analyticWithinAt, ContinuousLinearMap.analyticOn_uncurry_of_multilinear, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, AnalyticAt.pi, contMDiff_pi_space, MeasureTheory.charFunDual_pi, ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap, FormalMultilinearSeries.le_radius_pi, contDiffAt_pi, FormalMultilinearSeries.radius_pi_le, ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap, HasFPowerSeriesWithinOnBall.pi, contMDiffAt_pi_space, SmoothBumpCovering.embeddingPiTangent_coe, ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, NumberField.Units.basisOfIsMaxRank_fundSystem, AnalyticOnNhd.eval_mvPolynomial, ContinuousLinearMap.analyticAt_uncurry_of_multilinear, ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap, contDiff_pi, analyticAt_pi_iff, contDiffOn_apply, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, hasFTaylorSeriesUpToOn_pi, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, ZLattice.covolume_eq_det, contDiffOn_pi'
normedAddGroup 📖	CompOp	—
normedCommGroup 📖	CompOp	—
normedGroup 📖	CompOp	—
seminormedAddCommGroup 📖	CompOp	38 math math: Matrix.linfty_opNorm_diagonal, Matrix.norm_diagonal, ContinuousMultilinearMap.norm_iteratedFDerivComponent_le, Asymptotics.isBigOWith_pi, Matrix.norm_def, PiLp.norm_ofLp, ContinuousAlternatingMap.opNNNorm_pi, ContinuousAlternatingMap.piLIE_apply_apply, Asymptotics.isBigO_pi, Matrix.linfty_opNNNorm_eq_opNNNorm, ContinuousMultilinearMap.norm_image_sub_le, Matrix.linfty_opNNNorm_toMatrix, ContinuousMultilinearMap.opNorm_pi, AlternatingMap.norm_image_sub_le_of_bound, contDiff_apply_apply, Matrix.norm_replicateRow, ContinuousLinearMap.norm_single, MultilinearMap.norm_image_sub_le_of_bound, ContinuousAlternatingMap.piLIE_symm_apply_apply, ContinuousMultilinearMap.norm_iteratedFDeriv_le, ContinuousMultilinearMap.norm_iteratedFDeriv_le', Matrix.linfty_opNorm_replicateCol, ContinuousMultilinearMap.piₗᵢ_symm_apply, Matrix.linfty_opNorm_toMatrix, ContinuousMultilinearMap.opNNNorm_pi, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux, Matrix.linfty_opNorm_eq_opNorm, ContinuousLinearMap.norm_pi_le_of_le, ContinuousLinearMap.norm_single_le_one, ContinuousMultilinearMap.piₗᵢ_apply, Module.Basis.opNNNorm_le, Module.Basis.opNorm_le, ContinuousAlternatingMap.opNorm_pi, PiLp.norm_toLp, Matrix.norm_replicateCol, ContinuousAlternatingMap.norm_image_sub_le, normOneClass, Asymptotics.isLittleO_pi
seminormedAddGroup 📖	CompOp	36 math math: pi_nnnorm_le_iff, ContinuousAlternatingMap.opNNNorm_pi, nnnorm_single, MeasureTheory.Integrable.of_eval, Matrix.linfty_opNNNorm_mulVec, pi_nnnorm_lt_iff, pi_nnnorm_const, pi_norm_le_iff_of_nonneg, norm_le_pi_norm, enorm_single, Matrix.nnnorm_replicateRow, sum_nnnorm_apply_le_nnnorm, sum_norm_apply_le_norm, pi_norm_lt_iff, nnnorm_le_pi_nnnorm, NumberField.canonicalEmbedding.nnnorm_eq, norm_def, PiLp.nnnorm_toLp, MeasureTheory.memLp_pi_iff, instNormSMulClass, ContinuousMultilinearMap.opNNNorm_pi, Matrix.linfty_opNNNorm_replicateCol, nnnorm_def, pi_norm_le_iff_of_nonempty, MeasureTheory.MemLp.of_eval, pi_norm_const, Matrix.nnnorm_diagonal, MeasureTheory.integrable_pi_iff, Matrix.l2_opNNNorm_diagonal, Matrix.nnnorm_def, pi_nnnorm_const_le, Matrix.linfty_opNNNorm_diagonal, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, PiLp.nnnorm_ofLp, Matrix.nnnorm_replicateCol, pi_norm_const_le
seminormedCommGroup 📖	CompOp	—
seminormedGroup 📖	CompOp	15 math math: pi_nnnorm_lt_iff', norm_def', pi_nnnorm_const', sum_norm_apply_le_norm', nnnorm_def', pi_nnnorm_le_iff', sum_nnnorm_apply_le_nnnorm', pi_norm_const_le', pi_nnnorm_const_le', pi_norm_le_iff_of_nonneg', norm_le_pi_norm', pi_norm_const', pi_norm_lt_iff', nnnorm_le_pi_nnnorm', pi_norm_le_iff_of_nonempty'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enorm_single 📖	mathematical	—	ENorm.enorm NNNorm.toENorm SeminormedAddGroup.toNNNorm seminormedAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	nnnorm_single
nnnorm_def 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm seminormedAddGroup Finset.sup NNReal NNReal.instSemilatticeSup NNReal.instOrderBot Finset.univ	—	norm_nonneg
nnnorm_def' 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm seminormedGroup Finset.sup NNReal NNReal.instSemilatticeSup NNReal.instOrderBot Finset.univ	—	norm_nonneg'
nnnorm_single 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm seminormedAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	apply_single nnnorm_zero nnnorm_def single_apply Finset.sup_ite Finset.filter_eq' Finset.sup_singleton sup_of_le_left
norm_def 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm seminormedAddGroup NNReal.toReal Finset.sup NNReal NNReal.instSemilatticeSup NNReal.instOrderBot Finset.univ NNNorm.nnnorm SeminormedAddGroup.toNNNorm	—	—
norm_def' 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm seminormedGroup NNReal.toReal Finset.sup NNReal NNReal.instSemilatticeSup NNReal.instOrderBot Finset.univ NNNorm.nnnorm SeminormedGroup.toNNNorm	—	—
norm_single 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm normedAddCommGroup single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	nnnorm_single
sum_nnnorm_apply_le_nnnorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Finset.univ NNNorm.nnnorm SeminormedAddGroup.toNNNorm AddMonoid.toNSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card seminormedAddGroup	—	Eq.trans_le NNReal.coe_sum sum_norm_apply_le_norm
sum_nnnorm_apply_le_nnnorm' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Finset.univ NNNorm.nnnorm SeminormedGroup.toNNNorm AddMonoid.toNSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card seminormedGroup	—	Eq.trans_le NNReal.coe_sum sum_norm_apply_le_norm'
sum_norm_apply_le_norm 📖	mathematical	—	Real Real.instLE Finset.sum Real.instAddCommMonoid Finset.univ Norm.norm SeminormedAddGroup.toNorm AddMonoid.toNSMul Real.instAddMonoid Fintype.card seminormedAddGroup	—	Finset.sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_le_pi_norm
sum_norm_apply_le_norm' 📖	mathematical	—	Real Real.instLE Finset.sum Real.instAddCommMonoid Finset.univ Norm.norm SeminormedGroup.toNorm AddMonoid.toNSMul Real.instAddMonoid Fintype.card seminormedGroup	—	Finset.sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_le_pi_norm'

Prod

Definitions

Name	Category	Theorems
normedAddCommGroup 📖	CompOp	505 math math: contDiffAt_snd, TangentBundle.tangentMap_tangentBundle_pure, contMDiff_prod_assoc, mfderiv_prod_eq_add, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, instLieGroup, Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.mdifferentiableAt_proj, contDiff_fst, mdifferentiableAt_sub_section, ContinuousLinearMap.analyticWithinAt_bilinear, ContMDiffMul.prod, contDiff_prod_iff, MDifferentiableOn.finsum_section_of_locallyFinite, ModelWithCorners.range_prod, Bundle.contMDiffOn_zeroSection, MDifferentiableAt.clm_bundle_apply, ContDiffAt.implicitFunction_def, ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap, MDifferentiableAt.mfderiv_prod, MeasureTheory.contDiffOn_convolution_left_with_param, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContMDiffOn.prodMk, ContinuousMultilinearMap.analyticAt_uncurry_of_linear, analyticWithinAt_snd, contDiff_prodAssoc_symm, tangentMapWithin_prodSnd, ContMDiffOn.mlieBracketWithin_vectorField, ContMDiffWithinAt.mlieBracketWithin_vectorField, mdifferentiableAt_iff_localFrame_coeff, Bundle.Trivialization.contMDiffOn_section_baseSet_iff, ContDiffBumpBase.smooth, MDifferentiableOn.prodMk_space, MDifferentiableOn.smul_const_section, ContMDiffWithinAt.sub_section, Manifold.IsImmersionOfComplement.prodMap, contMDiff_addInvariantVectorField, HasStrictFDerivAt.rightFun_implicitFunctionDataOfProdDomain, mdifferentiableWithinAt_smul_const_section, ContinuousLinearMap.fpowerSeriesBilinear_apply_zero, mdifferentiableAt_add_section, HasMFDerivWithinAt.prodMk, ContMDiffAt.finsum_section_of_locallyFinite, contDiffWithinAt_fst, ContMDiffAdd.prod, ContMDiffMul.contMDiff_mul, Bundle.contMDiffWithinAt_zeroSection, mdifferentiableOn_snd, contMDiff_mul, contMDiff_mulInvariantVectorField, contMDiffWithinAt_snd, Bundle.Trivialization.contMDiffOn, contMDiffWithinAt_prod_iff, UniqueMDiffOn.prod, MDifferentiableWithinAt.finsum_section_of_locallyFinite, IsLocalFrameOn.contMDiffAt_of_coeff, contMDiff_equivTangentBundleProd_symm, contDiff_prodAssoc, mdifferentiableWithinAt_section, MDifferentiableWithinAt.prodMk_space, contMDiffOn_baseSet_iff_localFrame_coeff, ContinuousLinearMap.cpolynomialOn_uncurry_of_multilinear, ContMDiffWithinAt.add_section, ContDiffAt.prodMap, ContMDiffAt.add_section, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear, ContMDiffAdd.contMDiff_add, Manifold.IsSmoothEmbedding.prodMap, MDifferentiable.clm_bundle_apply₂, ContDiffAt.fst'', Manifold.IsImmersionAtOfComplement.prodMap, Diffeomorph.coe_prodCongr, hasMFDerivAt_fst, writtenInExtChart_prod, Bundle.contMDiffAt_zeroSection, ModelWithCorners.prod_target, contMDiffAt_mulInvariantVectorField, MDifferentiableAt.clm_prodMap, MDifferentiable.prodMap, equivTangentBundleProd_apply, contMDiffWithinAt_prod_module_iff, ContinuousLinearMap.analyticOn_bilinear, MDifferentiable.clm_bundle_apply, MDifferentiableWithinAt.clm_bundle_apply₂, HasMFDerivWithinAt.prodMap, mdifferentiableAt_addInvariantVectorField, ContDiff.prodMk, ContMDiff.sum_section_of_locallyFinite, ContMDiff.contMDiff_tangentMap, MDifferentiableAt.mpullback_vectorField, ContMDiffWithinAt.sum_section, MeasureTheory.charFunDual_prod, MeasureTheory.contDiffOn_convolution_right_with_param, MDifferentiableAt.sum_section, Module.Basis.prod_addHaar, mdifferentiableAt_fst, Bundle.Trivialization.mdifferentiableAt_section_iff, analyticOnNhd_snd, MDifferentiableOn.prodMk, mfderiv_prod_eq_add_comp, MDifferentiableAt.prodMap', NumberField.mixedEmbedding.fundamentalDomain_idealLattice, AnalyticWithinAt.prod, ContMDiffAt.prodMap, HasFPowerSeriesWithinOnBall.prod, ImplicitFunctionData.implicitFunction_def, mdifferentiableAt_totalSpace, mdifferentiableOn_fst, mdifferentiable_mulInvariantVectorField, contDiff_prodMk_right, contDiffOn_fst, mdifferentiableOn_prod_module_iff, ContDiff.prodMap, ContMDiffOn.finsum_section_of_locallyFinite, MDifferentiableOn.sum_section_of_locallyFinite, ContDiffWithinAt.prodMap, MDifferentiableAt.prodMk, ContMDiffWithinAt.neg_section, analyticAt_smul, Diffeomorph.prodCongr_symm, MeasureTheory.charFunDual_eq_prod_iff, ContMDiffWithinAt.mpullbackWithin_vectorField_inter, ContDiff.fst', mdifferentiableAt_hom_bundle, IsLocalFrameOn.mdifferentiableAt_of_coeff_aux, mdifferentiable_fst, ContDiffPointwiseHolderAt.snd, Bundle.Trivialization.continuousLinearEquivAt_prod, mdifferentiableWithinAt_neg_section, modelWithCorners_prod_coe, ContinuousLinearMap.analyticWithinAt_uncurry_of_multilinear, Bundle.TotalSpace.isManifold, ContMDiffAt.const_smul_section, IsBoundedBilinearMap.contDiff, MeasureTheory.hasFDerivAt_convolution_right_with_param, contMDiff_vectorSpace_iff_contDiff, mdifferentiableAt_snd, ContMDiffOn.mpullbackWithin_vectorField_inter, mfderiv_prodMap, ContMDiffAt.clm_apply_of_inCoordinates, ContMDiffWithinAt.prodMk_space, Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff, MDifferentiable.mpullback_vectorField, mdifferentiable_smul_const_section, Bundle.Trivialization.mdifferentiableOn_section_baseSet_iff, UniqueMDiffWithinAt.bundle_preimage', FiberBundle.exists_contMDiffOn_extend, AnalyticAt.prod, MDifferentiableAt.finsum_section_of_locallyFinite, IsContMDiffRiemannianBundle.exists_contMDiff, ModelWithCorners.prod_symm_apply, contMDiff_snd, ContMDiffAt.clm_bundle_apply, contMDiffAt_prod_iff, MDifferentiableOn.clm_prodMap, tangentMap_prodSnd, mdifferentiableAt_neg_section, Bundle.Trivialization.contMDiffOn_localFrame_baseSet, ContMDiffAt.prodMk_space, HasMFDerivAt.prodMap, MDifferentiableAt.clm_bundle_apply₂, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq, FiberBundle.writtenInExtChartAt_trivializationAt, IsLocalFrameOn.mdifferentiableOn_of_coeff, ModelWithCorners.prod_source, ContMDiffWithinAt.mpullback_vectorField_preimage, hasMFDerivWithinAt_fst, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq, WithLp.contDiff_toLp, snd_integral, NumberField.mixedEmbedding.covolume_idealLattice, MDifferentiableOn.prodMap, ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear, MDifferentiableAt.smul_section, mdifferentiableAt_prod_module_iff, ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq, FiberBundle.mdifferentiableAt_extend, swap_integral, ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear, ContDiffPointwiseHolderAt.prodMk, ContDiffWithinAt.prodMap', modelWithCorners_prod_coe_symm, MDifferentiable.prodMk_space, contMDiff_smul, MDifferentiableWithinAt.clm_apply_of_inCoordinates, Bundle.mdifferentiableWithinAt_proj, IsLocalFrameOn.contMDiffOn, ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear, MDifferentiableOn.clm_bundle_apply, MDifferentiableWithinAt.prodMk, Bundle.Trivialization.mdifferentiableOn_section_iff, tangentMapWithin_prodFst, ContMDiffWithinAt.finsum_section_of_locallyFinite, Bundle.contMDiffWithinAt_totalSpace, Diffeomorph.coe_prodComm, Bundle.Trivialization.contMDiffWithinAt_iff, mdifferentiableWithinAt_sub_section, Bundle.mdifferentiableOn_proj, contDiffOn_prod_iff, ContMDiffOn.prodMk_space, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, mdifferentiableWithinAt_add_section, ContMDiffWithinAt.mpullbackWithin_vectorField', ContinuousLinearMap.analyticOnNhd_bilinear, ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, equivTangentBundleProd_symm_apply_snd, MDifferentiable.sum_section, ContMDiffWithinAt.clm_bundle_apply₂, WithLp.contDiff_ofLp, iteratedFDerivWithin_prodMk, HasStrictFDerivAt.leftFun_implicitFunctionDataOfProdDomain, Module.Basis.prod_parallelepiped, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, ContMDiffOn.prodMap, MDifferentiable.sum_section_of_locallyFinite, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, FiberBundle.extChartAt, MDifferentiableWithinAt.sum_section_of_locallyFinite, ContMDiffAt.mlieBracket_vectorField, ContMDiffOn.add_section, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, mfderiv_prod_right, MDifferentiable.clm_prodMap, writtenInExtChartAt_prod, ContMDiff.finsum_section_of_locallyFinite, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, analyticAt_fst, Bundle.contMDiffWithinAt_proj, ModelWithCorners.boundary_of_boundaryless_left, modelWithCornersSelf_prod, Bundle.contMDiffAt_totalSpace, analyticWithinAt_fst, MDifferentiableAt.clm_apply_of_inCoordinates, MDifferentiableAt.prodMk_space, WithLp.analyticOn_toLp, ContDiffAt.snd', ContMDiffWithinAt.clm_bundle_apply, ContMDiff.clm_bundle_apply, contDiff_add, NumberField.mixedEmbedding.covolume_integerLattice, UniqueMDiffOn.tangentBundle_proj_preimage, MeasureTheory.average_pair, ContMDiff.clm_bundle_apply₂, mdifferentiable_snd, MDifferentiableOn.sum_section, mdifferentiableAt_prod_iff, MDifferentiable.prodMk, OpenPartialHomeomorph.extend_prod, FiberBundle.contMDiffAt_extend', contMDiffWithinAt_fst, ContinuousMultilinearMap.analyticOn_uncurry_of_linear, Bundle.contMDiffOn_proj, ContMDiffWithinAt.prodMk, Bundle.contMDiff_proj, HasFPowerSeriesWithinAt.prod, contMDiffOn_fst, ImplicitFunctionData.contDiffAt_implicitFunction, MDifferentiableAt.sum_section_of_locallyFinite, ContinuousLinearMap.analyticOnNhd_uncurry_of_multilinear, contDiffAt_inner, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, MDifferentiableOn.mpullback_vectorField_preimage, contMDiffOn_prod_iff, ContinuousLinearMap.hasFPowerSeriesAt_bilinear, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq, Manifold.IsImmersionAt.prodMap, IsManifold.prod, HasFTaylorSeriesUpToOn.prodMk, mfderivWithin_prodMap, integral_pair, SmoothBumpCovering.embeddingPiTangent_injOn, UniqueMDiffWithinAt.bundle_preimage, contMDiffAt_vectorSpace_iff_contDiffAt, ContMDiff.neg_section, Manifold.IsImmersion.prodMap, Bundle.mdifferentiableWithinAt_zeroSection, mfderiv_snd, ContMDiffAt.clm_prodMap, mdifferentiable_addInvariantVectorField, ContDiffAt.prodMap', VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, modelWithCorners_prod_toPartialEquiv, fst_integral, Bundle.Trivialization.contMDiff_iff, ContMDiffWithinAt.sum_section_of_locallyFinite, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, ExistsContDiffBumpBase.y_smooth, Bundle.contMDiff_zeroSection, contDiff_inner, ContDiff.mlieBracket_vectorField, FiberBundle.extChartAt_target, IsContDiffImplicitAt.contDiffAt, contMDiffAt_localFrame_of_mem, mdifferentiableWithinAt_snd, mfderiv_prodMk, hasMFDerivWithinAt_snd, contMDiff_prod_module_iff, mdifferentiableAt_section, Bundle.Trivialization.contMDiffAt_section_iff, Bundle.mdifferentiable_proj, ContMDiffWithinAt.clm_apply_of_inCoordinates, FiberBundle.writtenInExtChartAt_trivializationAt_symm, ModelWithCorners.boundary_of_boundaryless_right, ContMDiffAt.sub_section, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, ModelWithCorners.range_eq_univ_prod, ModelWithCorners.prod_apply, ContMDiff.clm_prodMap, SmoothBumpCovering.embeddingPiTangent_injective, MDifferentiableWithinAt.mpullback_vectorField_preimage, MDifferentiableWithinAt.clm_bundle_apply, ContMDiffSection.contMDiff, contDiff_mul, IsManifold.mem_maximalAtlas_prod, analyticOnNhd_fst, ContDiffAt.fst', contMDiff_equivTangentBundleProd, ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, HasFPowerSeriesOnBall.prod, UniqueMDiffOn.bundle_preimage, Bundle.Trivialization.contMDiffAt_iff, ContMDiffOn.const_smul_section, Bundle.contMDiffAt_section, Bundle.Trivialization.contMDiffWithinAt_section, ModelWithCorners.boundary_prod, ContinuousLinearMap.fpowerSeriesBilinear_radius, contDiff_smul, MDifferentiableOn.mpullbackWithin_vectorField_inter, ContMDiffAt.clm_bundle_apply₂, ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq, mDifferentiableOn_sub_section, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, contDiffOn_snd, ContinuousMultilinearMap.cpolynomialOn_uncurry_compContinuousLinearMap, mdifferentiable_prod_iff, ContinuousMultilinearMap.analyticWithinAt_uncurry_compContinuousLinearMap, mdifferentiableOn_prod_iff, Bundle.Trivialization.contMDiffOn_symm, mdifferentiableAt_mulInvariantVectorField, mfderivWithin_prodMk, contMDiffAt_iff_localFrame_coeff, contMDiffAt_prod_module_iff, ContMDiffOn.sum_section_of_locallyFinite, ContMDiffAt.prodMap', contDiffAt_prod_iff, iteratedFDeriv_prodMk, tangentMap_prodFst, ContMDiffCovariantDerivativeOn.contMDiff, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter, ContMDiffOn.contMDiffOn_tangentMapWithin, mdifferentiable_sub_section, ContMDiffWithinAt.const_smul_section, mdifferentiable_neg_section, ContMDiffWithinAt.prodMap', ContMDiffAt.sum_section_of_locallyFinite, mdifferentiableWithinAt_fst, MDifferentiable.finsum_section_of_locallyFinite, ContMDiffOn.mpullback_vectorField_preimage, IsLocalFrameOn.contMDiffOn_of_coeff, ModelWithCorners.BoundarylessManifold.prod, ContinuousLinearMap.analyticOn_uncurry_of_multilinear, contMDiff_add, HasFPowerSeriesAt.prod, FiberBundle.exists_mdifferentiableOn_extend, Diffeomorph.prodComm_symm, instLieAddGroup, HasMFDerivAt.prodMk, ContDiff.contDiff_fderiv_apply, ContMDiff.sub_section, MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq, FormalMultilinearSeries.radius_prod_eq_min, analyticAt_mul, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, ContMDiffWithinAt.mpullbackWithin_vectorField, ContMDiffAt.prodMk, Bundle.contMDiffAt_proj, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, ContMDiffWithinAt.clm_prodMap, MDifferentiableAt.smul_const_section, ContMDiffAt.mpullback_vectorField_preimage, ContMDiffOn.smul_section_of_tsupport, mdifferentiableWithinAt_prod_module_iff, ContMDiffWithinAt.smul_section, mdifferentiable_add_section, hasMFDerivAt_snd, ContDiff.snd', MDifferentiableOn.smul_section, MDifferentiableWithinAt.prodMap, ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap, Bundle.contMDiffWithinAt_section, Bundle.mdifferentiableOn_zeroSection, ContMDiffSection.mdifferentiable', contMDiff_tangentBundleModelSpaceHomeomorph_symm, IsContDiffImplicitAt.implicitFunction_def, mfderiv_fst, mfderivWithin_fst, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq, ContMDiffOn.sub_section, ContDiffOn.prodMk, ContMDiffSection.mdifferentiableAt, contDiffWithinAt_snd, ContinuousMultilinearMap.cpolynomialAt_uncurry_compContinuousLinearMap, MDifferentiableOn.smul_section_of_tsupport, ContMDiff.add_section, ContMDiffOn.clm_prodMap, contDiffWithinAt_prod_iff, Bundle.Prod.contMDiffVectorBundle, ContMDiffOn.sum_section, AnalyticOn.prod, ContMDiffOn.neg_section, UniqueMDiffWithinAt.prod, mdifferentiable_prod_module_iff, equivTangentBundleProd_symm_apply_proj, ContMDiffSection.mdifferentiable, HasStrictFDerivAt.pt_implicitFunctionDataOfProdDomain, contDiff_snd, Bundle.Trivialization.contMDiffOn_iff, ContMDiff.prodMk_space, ContMDiffWithinAt.prodMap, mdifferentiable_smul_section, ContDiffWithinAt.prodMk, Bundle.mdifferentiable_zeroSection, Bundle.Trivialization.mdifferentiableWithinAt_section_iff, contMDiffAt_fst, mdifferentiableWithinAt_prod_iff, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, IsLocalFrameOn.mdifferentiableAt_of_coeff, ContinuousLinearMap.analyticAt_bilinear, contDiffOn_fderivWithin_apply, ContMDiffAt.sum_section, ContMDiff.const_smul_section, ContDiffAt.prodMk, tangentMap_prod_right, contMDiffOn_vectorSpace_iff_contDiffOn, ContDiffOn.prodMap, contDiffAt_fst, ContMDiffOn.clm_bundle_apply, Bundle.Trivialization.contMDiffOn_section_iff, tangentMap_prod_left, mdifferentiableOn_add_section, SmoothBumpCovering.embeddingPiTangent_coe, ContMDiffSection.contMDiff_toFun, ContMDiffAt.smul_section, ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, contDiffGroupoid_prod, ModelWithCorners.interior_prod, contMDiffOn_snd, ContinuousLinearMap.analyticAt_uncurry_of_multilinear, mfderiv_prod_left, ContinuousMultilinearMap.analyticOn_uncurry_compContinuousLinearMap, MeasureTheory.contDiffOn_convolution_right_with_param_aux, MDifferentiableWithinAt.clm_prodMap, contMDiffOn_prod_module_iff, ContMDiffAt.neg_section, ContDiffPointwiseHolderAt.fst, MDifferentiableWithinAt.prodMap', mdifferentiableWithinAt_hom_bundle, IsLocalFrameOn.contMDiffAt_of_coeff_aux, ContDiffAt.snd'', Bundle.Trivialization.contMDiffOn_symm_trans, Real.contDiffAt_rpow_of_ne, contMDiff_fst, Bundle.mdifferentiableAt_zeroSection, boundary_product, contDiff_prodMk_left, MDifferentiableAt.prodMap, ContMDiff.sum_section, VectorBundle.prod, mdifferentiableOn_neg_section, Bundle.Trivialization.mdifferentiableAt_totalSpace_iff, ContMDiff.prodMap, contMDiff_snd_tangentBundle_modelSpace, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq', contMDiffWithinAt_hom_bundle, ContinuousLinearMap.fpowerSeriesBilinear_apply_one, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, mfderivWithin_snd, analyticOn_snd, MDifferentiableOn.clm_bundle_apply₂, contMDiffAt_snd, ContMDiffOn.clm_bundle_apply₂, mfderiv_prod_eq_add_apply, extChartAt_prod, ContMDiff.mpullback_vectorField, analyticOn_fst, Bundle.Trivialization.Bundle.Trivialization.mdifferentiable, MDifferentiableWithinAt.sum_section, WithLp.analyticOn_ofLp, ContMDiff.smul_section, HasStrictFDerivAt.implicitFunctionOfProdDomain_def, analyticAt_snd, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin, Manifold.LiftSourceTargetPropertyAt.prodMap, MDifferentiableWithinAt.smul_section, ContMDiffOn.smul_section, contMDiffOn_iff_localFrame_coeff, ProbabilityTheory.indepFun_iff_charFunDual_prod, AnalyticOnNhd.prod, ContMDiff.prodMk
normedAddGroup 📖	CompOp	—
normedCommGroup 📖	CompOp	—
normedGroup 📖	CompOp	—
seminormedAddCommGroup 📖	CompOp	52 math math: ContinuousAlternatingMap.opNorm_prod, ContinuousLinearMap.opNorm_prod, ContinuousLinearMap.norm_inr_le_one, IsBoundedLinearMap.fst, norm_jacobiTheta₂_term_fderiv_ge, ContinuousLinearMap.norm_inl_le_one, ContinuousLinearMap.norm_fst_le, ContinuousLinearMap.opNNNorm_prod, MDifferentiableAt.clm_prodMap, ContinuousAffineMap.decompLinearIsometryEquiv_symm_apply, LinearIsometryEquiv.symm_prodComm, MeasureTheory.hasFDerivAt_convolution_right_with_param, LinearIsometryEquiv.coe_prodAssoc_symm, MDifferentiableOn.clm_prodMap, ContinuousMultilinearMap.prodL_apply, ContinuousAffineMap.decompLinearIsometryEquiv_symm_contLinear, IsBoundedBilinearMap.isBoundedLinearMap_deriv, IsBoundedLinearMap.snd, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, ContinuousLinearMap.norm_inr, MDifferentiable.clm_prodMap, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, LinearIsometry.inr_apply, ContinuousMultilinearMap.opNNNorm_prod, SmoothBumpCovering.embeddingPiTangent_injOn, ContMDiffAt.clm_prodMap, ContinuousAffineMap.snd_decompLinearIsometryEquiv, LinearIsometryEquiv.prodComm_symm_apply, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, ContinuousLinearMap.norm_fst, ContMDiff.clm_prodMap, SmoothBumpCovering.embeddingPiTangent_injective, ContinuousMultilinearMap.prodL_symm_apply, ContinuousLinearMap.norm_inl, ContinuousAlternatingMap.prodLIE_apply, LinearIsometry.inl_apply, ContinuousAffineMap.fst_decompLinearIsometryEquiv, ContMDiffWithinAt.clm_prodMap, ContinuousLinearMap.norm_snd_le, LinearIsometryEquiv.prodComm_apply, ContMDiffOn.clm_prodMap, ContinuousLinearMap.norm_snd, ContinuousAffineMap.toConstProdContinuousLinearMap_fst, ContinuousMultilinearMap.opNorm_prod, SmoothBumpCovering.embeddingPiTangent_coe, ContinuousAlternatingMap.prodLIE_symm_apply, ContinuousAlternatingMap.opNNNorm_prod, MDifferentiableWithinAt.clm_prodMap, isBoundedLinearMap_prod_multilinear, LinearIsometryEquiv.coe_prodAssoc, norm_jacobiTheta₂_term_fderiv_le, ContinuousAffineMap.toConstProdContinuousLinearMap_snd
seminormedAddGroup 📖	CompOp	14 math math: WithLp.prod_nnnorm_ofLp, DoubleCentralizer.nnnorm_def', Unitization.nnnorm_def, ContinuousLinearMap.opNNNorm_prod, MeasureTheory.integrable_prod, DoubleCentralizer.nnnorm_def, MeasureTheory.memLp_prod_iff, nnnorm_def, MeasureTheory.MemLp.of_fst_snd, MeasureTheory.SimpleFunc.integrable_pair, WithLp.prod_nnnorm_toLp, MeasureTheory.Integrable.prodMk, nnnorm_mk, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace
seminormedCommGroup 📖	CompOp	—
seminormedGroup 📖	CompOp	2 math math: nnnorm_mk', nnnorm_def'
toNorm 📖	CompOp	42 math math: ContinuousLinearMap.opNorm_prod, Asymptotics.IsLittleO.prod_rightr, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, Asymptotics.isLittleO_prod_left, Asymptotics.isBigO_prod_left, NumberField.mixedEmbedding.norm_le_convexBodySumFun, HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, WithLp.prod_norm_toLp, DoubleCentralizer.norm_def', Asymptotics.isBigO_fst_prod, IsBoundedBilinearMap.isBigO', DoubleCentralizer.norm_def, Complex.equivRealProd_apply_le', Asymptotics.isBigO_fst_prod', Asymptotics.IsLittleO.prod_left, WithLp.prod_norm_ofLp, norm_snd_le, HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub, HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal, norm_prod_le_iff, Asymptotics.isBigO_snd_prod', norm_def, Asymptotics.isBigO_snd_prod, Unitization.norm_def, instNormSMulClass, norm_mk, Asymptotics.IsBigOWith.prod_rightl, Asymptotics.isBigOWith_prod_left, WithCStarModule.norm_equiv_le_norm_prod, Asymptotics.IsBigOWith.prod_left, Asymptotics.IsBigO.prod_rightl, HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub, Asymptotics.IsBigO.prod_rightr, normOneClass, Asymptotics.isBigOWith_snd_prod, Asymptotics.IsLittleO.prod_rightl, Asymptotics.IsBigO.prod_left, Asymptotics.IsBigOWith.prod_rightr, Asymptotics.isBigOWith_fst_prod, Asymptotics.IsBigOWith.prod_left_same, Complex.equivRealProd_apply_le, norm_fst_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_def 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm seminormedAddGroup NNReal SemilatticeSup.toMax NNReal.instSemilatticeSup	—	—
nnnorm_def' 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm seminormedGroup NNReal SemilatticeSup.toMax NNReal.instSemilatticeSup	—	—
nnnorm_mk 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm seminormedAddGroup NNReal SemilatticeSup.toMax NNReal.instSemilatticeSup	—	—
nnnorm_mk' 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm seminormedGroup NNReal SemilatticeSup.toMax NNReal.instSemilatticeSup	—	—
norm_def 📖	mathematical	—	Norm.norm toNorm Real Real.instMax	—	—
norm_mk 📖	mathematical	—	Norm.norm toNorm Real Real.instMax	—	—

ULift

Definitions

Name	Category	Theorems
nnnorm 📖	CompOp	3 math math: nnnorm_up, nnnorm_def, nnnorm_down
norm 📖	CompOp	5 math math: norm_up, norm_down, normOneClass, norm_def, instNormSMulClass
normedAddCommGroup 📖	CompOp	—
normedAddGroup 📖	CompOp	—
normedCommGroup 📖	CompOp	—
normedGroup 📖	CompOp	—
seminormedAddCommGroup 📖	CompOp	—
seminormedAddGroup 📖	CompOp	—
seminormedCommGroup 📖	CompOp	—
seminormedGroup 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_def 📖	mathematical	—	NNNorm.nnnorm nnnorm	—	—
nnnorm_down 📖	mathematical	—	NNNorm.nnnorm nnnorm	—	—
nnnorm_up 📖	mathematical	—	NNNorm.nnnorm nnnorm	—	—
norm_def 📖	mathematical	—	Norm.norm norm	—	—
norm_down 📖	mathematical	—	Norm.norm norm	—	—
norm_up 📖	mathematical	—	Norm.norm norm	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_le_pi_nnnorm 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm Pi.seminormedAddGroup	—	norm_le_pi_norm
nnnorm_le_pi_nnnorm' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedGroup.toNNNorm Pi.seminormedGroup	—	norm_le_pi_norm'
nnnorm_ofAdd 📖	mathematical	—	NNNorm.nnnorm Multiplicative Multiplicative.toNNNorm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	—
nnnorm_ofDual 📖	mathematical	—	NNNorm.nnnorm DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toNNNorm	—	—
nnnorm_ofMul 📖	mathematical	—	NNNorm.nnnorm Additive Additive.toNNNorm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	—
nnnorm_toAdd 📖	mathematical	—	NNNorm.nnnorm DFunLike.coe Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd Multiplicative.toNNNorm	—	—
nnnorm_toDual 📖	mathematical	—	NNNorm.nnnorm OrderDual OrderDual.toNNNorm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	—
nnnorm_toMul 📖	mathematical	—	NNNorm.nnnorm DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.toMul Additive.toNNNorm	—	—
norm_fst_le 📖	mathematical	—	Real Real.instLE Norm.norm Prod.toNorm	—	le_max_left
norm_le_pi_norm 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Pi.seminormedAddGroup	—	pi_norm_le_iff_of_nonneg norm_nonneg le_rfl
norm_le_pi_norm' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Pi.seminormedGroup	—	pi_norm_le_iff_of_nonneg' norm_nonneg' le_rfl
norm_ofAdd 📖	mathematical	—	Norm.norm Multiplicative Multiplicative.toNorm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	—
norm_ofDual 📖	mathematical	—	Norm.norm DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toNorm	—	—
norm_ofMul 📖	mathematical	—	Norm.norm Additive Additive.toNorm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	—
norm_prod_le_iff 📖	mathematical	—	Real Real.instLE Norm.norm Prod.toNorm	—	max_le_iff
norm_snd_le 📖	mathematical	—	Real Real.instLE Norm.norm Prod.toNorm	—	le_max_right
norm_toAdd 📖	mathematical	—	Norm.norm DFunLike.coe Equiv Multiplicative EquivLike.toFunLike Equiv.instEquivLike Multiplicative.toAdd Multiplicative.toNorm	—	—
norm_toDual 📖	mathematical	—	Norm.norm OrderDual OrderDual.toNorm DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	—
norm_toMul 📖	mathematical	—	Norm.norm DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.toMul Additive.toNorm	—	—
pi_nnnorm_const 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm Pi.seminormedAddGroup	—	NNReal.eq pi_norm_const
pi_nnnorm_const' 📖	mathematical	—	NNNorm.nnnorm SeminormedGroup.toNNNorm Pi.seminormedGroup	—	NNReal.eq pi_norm_const'
pi_nnnorm_const_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm Pi.seminormedAddGroup	—	pi_norm_const_le
pi_nnnorm_const_le' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedGroup.toNNNorm Pi.seminormedGroup	—	pi_norm_const_le'
pi_nnnorm_le_iff 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm Pi.seminormedAddGroup	—	pi_norm_le_iff_of_nonneg NNReal.coe_nonneg
pi_nnnorm_le_iff' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedGroup.toNNNorm Pi.seminormedGroup	—	pi_norm_le_iff_of_nonneg' NNReal.coe_nonneg
pi_nnnorm_lt_iff 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedAddGroup.toNNNorm Pi.seminormedAddGroup	—	pi_norm_lt_iff
pi_nnnorm_lt_iff' 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNNorm.nnnorm SeminormedGroup.toNNNorm Pi.seminormedGroup	—	pi_norm_lt_iff'
pi_norm_const 📖	mathematical	—	Norm.norm SeminormedAddGroup.toNorm Pi.seminormedAddGroup	—	dist_zero_right dist_pi_const
pi_norm_const' 📖	mathematical	—	Norm.norm SeminormedGroup.toNorm Pi.seminormedGroup	—	dist_pi_const
pi_norm_const_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Pi.seminormedAddGroup	—	pi_norm_le_iff_of_nonneg norm_nonneg le_rfl
pi_norm_const_le' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Pi.seminormedGroup	—	pi_norm_le_iff_of_nonneg' norm_nonneg' le_rfl
pi_norm_le_iff_of_nonempty 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Pi.seminormedAddGroup	—	pi_norm_le_iff_of_nonneg LE.le.trans norm_nonneg
pi_norm_le_iff_of_nonempty' 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedGroup.toNorm Pi.seminormedGroup	—	pi_norm_le_iff_of_nonneg' LE.le.trans norm_nonneg'
pi_norm_le_iff_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Pi.seminormedAddGroup	—	dist_zero_right dist_pi_le_iff
pi_norm_le_iff_of_nonneg' 📖	mathematical	Real Real.instLE Real.instZero	Real Real.instLE Norm.norm SeminormedGroup.toNorm Pi.seminormedGroup	—	dist_pi_le_iff
pi_norm_lt_iff 📖	mathematical	Real Real.instLT Real.instZero	Real Real.instLT Norm.norm SeminormedAddGroup.toNorm Pi.seminormedAddGroup	—	dist_zero_right dist_pi_lt_iff
pi_norm_lt_iff' 📖	mathematical	Real Real.instLT Real.instZero	Real Real.instLT Norm.norm SeminormedGroup.toNorm Pi.seminormedGroup	—	dist_pi_lt_iff

---

← Back to Index