Documentation Verification Report

LpEquiv

📁 Source: Mathlib/Analysis/Normed/Lp/LpEquiv.lean

Statistics

Metric	Count
Definitions `lpBCF`, `lpPiLp`, `lpBCF`, `lpPiLp`, `lpBCF`, `lpBCFₗᵢ`, `lpPiLpₗᵢ`	7
Theorems `all`, `coe_addEquiv_lpBCF`, `coe_addEquiv_lpBCF_symm`, `coe_addEquiv_lpPiLp`, `coe_addEquiv_lpPiLp_symm`, `coe_algEquiv_lpBCF`, `coe_algEquiv_lpBCF_symm`, `coe_equiv_lpPiLp`, `coe_equiv_lpPiLp_symm`, `coe_lpBCFₗᵢ`, `coe_lpBCFₗᵢ_symm`, `coe_lpPiLpₗᵢ`, `coe_lpPiLpₗᵢ_symm`, `coe_ringEquiv_lpBCF`, `coe_ringEquiv_lpBCF_symm`, `equiv_lpPiLp_norm`	16
Total	23

AddEquiv

Definitions

Name	Category	Theorems
`lpBCF` 📖	CompOp	2 math math: `coe_addEquiv_lpBCF_symm`, `coe_addEquiv_lpBCF`
`lpPiLp` 📖	CompOp	2 math math: `coe_addEquiv_lpPiLp_symm`, `coe_addEquiv_lpPiLp`

AlgEquiv

Definitions

Name	Category	Theorems
`lpBCF` 📖	CompOp	2 math math: `coe_algEquiv_lpBCF_symm`, `coe_algEquiv_lpBCF`

Equiv

Definitions

Name	Category	Theorems
`lpPiLp` 📖	CompOp	3 math math: `coe_equiv_lpPiLp_symm`, `coe_equiv_lpPiLp`, `equiv_lpPiLp_norm`

Memℓp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`all` 📖	mathematical	—	`Memℓp`	—	`ENNReal.trichotomy` `memℓp_zero_iff` `Set.toFinite` `Subtype.finite` `memℓp_infty_iff` `Set.Finite.bddAbove` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Finite.Set.finite_range` `nonempty_fintype` `memℓp_gen` `hasSum_fintype` `SummationFilter.instLeAtTopUnconditional`

RingEquiv

Definitions

Name	Category	Theorems
`lpBCF` 📖	CompOp	2 math math: `coe_ringEquiv_lpBCF`, `coe_ringEquiv_lpBCF_symm`

(root)

Definitions

Name	Category	Theorems
`lpBCFₗᵢ` 📖	CompOp	2 math math: `coe_lpBCFₗᵢ`, `coe_lpBCFₗᵢ_symm`
`lpPiLpₗᵢ` 📖	CompOp	2 math math: `coe_lpPiLpₗᵢ`, `coe_lpPiLpₗᵢ_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_addEquiv_lpBCF` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoundedContinuousFunction.instFunLike` `AddEquiv` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `AddSubgroup.add` `BoundedContinuousFunction.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.lpBCF`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`coe_addEquiv_lpBCF_symm` 📖	mathematical	—	`PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `DFunLike.coe` `AddEquiv` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoundedContinuousFunction.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `AddSubgroup.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `AddEquiv.lpBCF` `BoundedContinuousFunction.instFunLike`	—	`instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`coe_addEquiv_lpPiLp` 📖	mathematical	—	`WithLp.ofLp` `DFunLike.coe` `AddEquiv` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `PiLp` `AddSubgroup.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.lpPiLp`	—	—
`coe_addEquiv_lpPiLp_symm` 📖	mathematical	—	`PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `DFunLike.coe` `AddEquiv` `PiLp` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `AddSubgroup.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `AddEquiv.lpPiLp` `WithLp.ofLp`	—	—
`coe_algEquiv_lpBCF` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `BoundedContinuousFunction.instFunLike` `AlgEquiv` `PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `lp.inftyRing` `BoundedContinuousFunction.instSemiring` `NormedRing.toRing` `instBoundedMul` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `IsTopologicalSemiring.toContinuousMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `NormedAlgebra.toAlgebra` `lp.inftyNormedRing` `lp.inftyNormedAlgebra` `BoundedContinuousFunction.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.lpBCF`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd`
`coe_algEquiv_lpBCF_symm` 📖	mathematical	—	`PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `DFunLike.coe` `AlgEquiv` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `BoundedContinuousFunction.instSemiring` `Ring.toSemiring` `NormedRing.toRing` `instBoundedMul` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `IsTopologicalSemiring.toContinuousMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `lp.inftyRing` `BoundedContinuousFunction.instAlgebra` `NormedAlgebra.toAlgebra` `lp.inftyNormedRing` `lp.inftyNormedAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `AlgEquiv.lpBCF` `BoundedContinuousFunction.instFunLike`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd`
`coe_equiv_lpPiLp` 📖	mathematical	—	`WithLp.ofLp` `DFunLike.coe` `Equiv` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `PiLp` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.lpPiLp`	—	—
`coe_equiv_lpPiLp_symm` 📖	mathematical	—	`PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `DFunLike.coe` `Equiv` `PiLp` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.lpPiLp` `WithLp.ofLp`	—	—
`coe_lpBCFₗᵢ` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoundedContinuousFunction.instFunLike` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `lp.normedAddCommGroup` `fact_one_le_top_ennreal` `BoundedContinuousFunction.instSeminormedAddCommGroup` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `NormedSpace.toIsBoundedSMul` `BoundedContinuousFunction.instModule` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `lpBCFₗᵢ`	—	`RingHomInvPair.ids` `fact_one_le_top_ennreal` `NormedSpace.toIsBoundedSMul`
`coe_lpBCFₗᵢ_symm` 📖	mathematical	—	`PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BoundedContinuousFunction.instSeminormedAddCommGroup` `lp.normedAddCommGroup` `fact_one_le_top_ennreal` `BoundedContinuousFunction.instModule` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `NormedSpace.toIsBoundedSMul` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `lpBCFₗᵢ` `BoundedContinuousFunction.instFunLike`	—	`RingHomInvPair.ids` `fact_one_le_top_ennreal` `NormedSpace.toIsBoundedSMul`
`coe_lpPiLpₗᵢ` 📖	mathematical	—	`WithLp.ofLp` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `PiLp` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `PiLp.seminormedAddCommGroup` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `NormedSpace.toIsBoundedSMul` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `lpPiLpₗᵢ`	—	`RingHomInvPair.ids` `NormedSpace.toIsBoundedSMul`
`coe_lpPiLpₗᵢ_symm` 📖	mathematical	—	`PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiLp` `PiLp.seminormedAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `lp.normedAddCommGroup` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `lp.instModuleSubtypePreLpMemAddSubgroup` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedSpace.toIsBoundedSMul` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `lpPiLpₗᵢ` `WithLp.ofLp`	—	`RingHomInvPair.ids` `NormedSpace.toIsBoundedSMul`
`coe_ringEquiv_lpBCF` 📖	mathematical	—	`DFunLike.coe` `BoundedContinuousFunction` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `BoundedContinuousFunction.instFunLike` `RingEquiv` `PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `lp.instMulSubtypePreLpMemAddSubgroupTopENNReal` `BoundedContinuousFunction.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `AddSubgroup.add` `BoundedContinuousFunction.instAdd` `Distrib.toAdd` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.lpBCF`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd`
`coe_ringEquiv_lpBCF_symm` 📖	mathematical	—	`PreLp` `NonUnitalNormedRing.toNormedAddCommGroup` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `Top.top` `ENNReal` `instTopENNReal` `DFunLike.coe` `RingEquiv` `BoundedContinuousFunction` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `BoundedContinuousFunction.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `lp.instMulSubtypePreLpMemAddSubgroupTopENNReal` `BoundedContinuousFunction.instAdd` `Distrib.toAdd` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsTopologicalSemiring.toContinuousAdd` `AddSubgroup.add` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `RingEquiv.lpBCF` `BoundedContinuousFunction.instFunLike`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalSemiring.toContinuousAdd`
`equiv_lpPiLp_norm` 📖	mathematical	—	`Norm.norm` `PiLp` `PiLp.instNorm` `NormedAddCommGroup.toNorm` `DFunLike.coe` `Equiv` `PreLp` `AddSubgroup` `AddCommGroup.toAddGroup` `instAddCommGroupPreLp` `SetLike.instMembership` `AddSubgroup.instSetLike` `lp` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.lpPiLp` `Finite.of_fintype` `lp.instNormSubtypePreLpMemAddSubgroup`	—	`Finite.of_fintype` `ENNReal.trichotomy` `Set.toFinite` `Subtype.finite` `Memℓp.finite_dsupport` `lp.memℓp` `PiLp.norm_eq_card` `Set.Finite.toFinset.congr_simp` `lp.norm_eq_card_dsupport` `PiLp.norm_eq_ciSup` `lp.norm_eq_ciSup` `PiLp.norm_eq_sum` `lp.norm_eq_tsum_rpow` `tsum_fintype` `SummationFilter.instLeAtTopUnconditional`

---

← Back to Index