Documentation Verification Report

Basic

📁 Source: Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean

Statistics

Metric	Count
Definitions `instAddActionSubtypeAEEqFunMemAddAddSubgroupLp`, `instVAddSubtypeAEEqFunMemAddAddSubgroupLp`, `instDistribMulActionSubtypeAEEqFunMemAddSubgroupLp`, `instDistribSMulSubtypeAEEqFunMemAddSubgroupLp`, `instMulActionSubtypeAEEqFunMemAddSubgroupLp`, `instSMulSubtypeAEEqFunMemAddSubgroupLp`	6
Theorems `dist_vadd_Lp`, `edist_vadd_Lp`, `instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp`, `mk_vadd_indicatorConstLp`, `mk_vadd_toLp`, `nnnorm_vadd_Lp`, `norm_vadd_Lp`, `vadd_Lp_add`, `vadd_Lp_ae_eq`, `vadd_Lp_const`, `vadd_Lp_neg`, `vadd_Lp_sub`, `vadd_Lp_val`, `vadd_Lp_zero`, `dist_smul_Lp`, `edist_smul_Lp`, `instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp`, `instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp`, `instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1`, `instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2`, `mk_smul_indicatorConstLp`, `mk_smul_toLp`, `nnnorm_smul_Lp`, `norm_smul_Lp`, `smul_Lp_add`, `smul_Lp_ae_eq`, `smul_Lp_const`, `smul_Lp_neg`, `smul_Lp_sub`, `smul_Lp_val`, `smul_Lp_zero`	31
Total	37

DomAddAct

Definitions

Name	Category	Theorems
`instAddActionSubtypeAEEqFunMemAddAddSubgroupLp` 📖	CompOp	—
`instVAddSubtypeAEEqFunMemAddAddSubgroupLp` 📖	CompOp	15 math math: `mk_vadd_indicatorConstLp`, `instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp`, `vadd_Lp_add`, `norm_vadd_Lp`, `vadd_Lp_ae_eq`, `vadd_Lp_sub`, `MeasureTheory.Lp.instContinuousVAddDomAddAct`, `vadd_Lp_neg`, `edist_vadd_Lp`, `mk_vadd_toLp`, `vadd_Lp_const`, `dist_vadd_Lp`, `vadd_Lp_zero`, `nnnorm_vadd_Lp`, `vadd_Lp_val`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_vadd_Lp` 📖	mathematical	—	`Dist.dist` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instDist` `HVAdd.hVAdd` `DomAddAct` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `vadd_Lp_sub` `norm_vadd_Lp`
`edist_vadd_Lp` 📖	mathematical	—	`EDist.edist` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instEDist` `HVAdd.hVAdd` `DomAddAct` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Lp.edist_dist` `dist_vadd_Lp`
`instIsIsometricVAddSubtypeAEEqFunMemAddAddSubgroupLp` 📖	mathematical	—	`IsIsometricVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `MeasureTheory.Lp.instNormedAddCommGroup` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `edist_vadd_Lp`
`mk_vadd_indicatorConstLp` 📖	mathematical	`MeasurableSet`	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasureTheory.indicatorConstLp` `Set.preimage` `MeasurableSet.preimage` `MeasurableConstVAdd.measurable_const_vadd`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`mk_vadd_toLp` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasureTheory.MemLp.toLp` `MeasureTheory.MemLp.comp_measurePreserving` `MeasureTheory.measurePreserving_vadd`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`nnnorm_vadd_Lp` 📖	mathematical	—	`NNNorm.nnnorm` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNNNorm` `HVAdd.hVAdd` `DomAddAct` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `NNReal.eq` `MeasureTheory.Lp.norm_compMeasurePreserving`
`norm_vadd_Lp` 📖	mathematical	—	`Norm.norm` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNorm` `HVAdd.hVAdd` `DomAddAct` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Lp.norm_compMeasurePreserving`
`vadd_Lp_add` 📖	mathematical	—	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `AddSubgroup.add`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`vadd_Lp_ae_eq` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `HVAdd.hVAdd` `DomAddAct` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Lp.coeFn_compMeasurePreserving`
`vadd_Lp_const` 📖	mathematical	—	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddMonoidHom.instFunLike` `MeasureTheory.Lp.const`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`vadd_Lp_neg` 📖	mathematical	—	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `AddSubgroup.neg`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`vadd_Lp_sub` 📖	mathematical	—	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `AddSubgroup.sub`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`vadd_Lp_val` 📖	mathematical	—	`MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `HVAdd.hVAdd` `DomAddAct` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `instVAddAEEqFun`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`vadd_Lp_zero` 📖	mathematical	—	`HVAdd.hVAdd` `DomAddAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instHVAdd` `instVAddSubtypeAEEqFunMemAddAddSubgroupLp` `AddSubgroup.zero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`

DomMulAct

Definitions

Name	Category	Theorems
`instDistribMulActionSubtypeAEEqFunMemAddSubgroupLp` 📖	CompOp	—
`instDistribSMulSubtypeAEEqFunMemAddSubgroupLp` 📖	CompOp	—
`instMulActionSubtypeAEEqFunMemAddSubgroupLp` 📖	CompOp	—
`instSMulSubtypeAEEqFunMemAddSubgroupLp` 📖	CompOp	18 math math: `instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1`, `smul_Lp_sub`, `edist_smul_Lp`, `mk_smul_toLp`, `instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2`, `mk_smul_indicatorConstLp`, `smul_Lp_neg`, `norm_smul_Lp`, `dist_smul_Lp`, `instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp`, `smul_Lp_zero`, `smul_Lp_ae_eq`, `instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp`, `nnnorm_smul_Lp`, `smul_Lp_const`, `smul_Lp_val`, `MeasureTheory.Lp.instContinuousSMulDomMulAct`, `smul_Lp_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_smul_Lp` 📖	mathematical	—	`Dist.dist` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instDist` `DomMulAct` `instSMulSubtypeAEEqFunMemAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `norm_smul_Lp`
`edist_smul_Lp` 📖	mathematical	—	`EDist.edist` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instEDist` `DomMulAct` `instSMulSubtypeAEEqFunMemAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Lp.edist_dist` `dist_smul_Lp`
`instIsIsometricSMulSubtypeAEEqFunMemAddSubgroupLp` 📖	mathematical	—	`IsIsometricSMul` `DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `MeasureTheory.Lp.instNormedAddCommGroup` `instSMulSubtypeAEEqFunMemAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `edist_smul_Lp`
`instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp`	—	`Function.Injective.smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instSMulCommClassAEEqFun_2` `Subtype.val_injective`
`instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `AddSubgroup.toAddCommGroup` `MeasureTheory.AEEqFun.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule`	—	`Function.Injective.smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instSMulCommClassAEEqFun` `Subtype.val_injective`
`instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_2` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `AddSubgroup.toAddCommGroup` `MeasureTheory.AEEqFun.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `instSMulSubtypeAEEqFunMemAddSubgroupLp`	—	`SMulCommClass.symm` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instSMulCommClassSubtypeAEEqFunMemAddSubgroupLp_1`
`mk_smul_indicatorConstLp` 📖	mathematical	`MeasurableSet`	`DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasureTheory.indicatorConstLp` `Set.preimage` `MeasurableSet.preimage` `MeasurableConstSMul.measurable_const_smul`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`mk_smul_toLp` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`DomMulAct` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasureTheory.MemLp.toLp` `MeasureTheory.MemLp.comp_measurePreserving` `MeasureTheory.measurePreserving_smul`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`nnnorm_smul_Lp` 📖	mathematical	—	`NNNorm.nnnorm` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNNNorm` `DomMulAct` `instSMulSubtypeAEEqFunMemAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `NNReal.eq` `MeasureTheory.Lp.norm_compMeasurePreserving`
`norm_smul_Lp` 📖	mathematical	—	`Norm.norm` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNorm` `DomMulAct` `instSMulSubtypeAEEqFunMemAddSubgroupLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Lp.norm_compMeasurePreserving`
`smul_Lp_add` 📖	mathematical	—	`DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `AddSubgroup.add`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`smul_Lp_ae_eq` 📖	mathematical	—	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `DomMulAct` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Lp.coeFn_compMeasurePreserving`
`smul_Lp_const` 📖	mathematical	—	`DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddMonoidHom.instFunLike` `MeasureTheory.Lp.const`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`smul_Lp_neg` 📖	mathematical	—	`DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `AddSubgroup.neg`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`smul_Lp_sub` 📖	mathematical	—	`DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `AddSubgroup.sub`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`smul_Lp_val` 📖	mathematical	—	`MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `DomMulAct` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `instSMulAEEqFun`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`
`smul_Lp_zero` 📖	mathematical	—	`DomMulAct` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSMulSubtypeAEEqFunMemAddSubgroupLp` `AddSubgroup.zero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup`

---

← Back to Index