Documentation Verification Report

HolderNorm

📁 Source: Mathlib/Topology/MetricSpace/HolderNorm.lean

Statistics

Metric	Count
Definitions `MemHolder`, `eHolderNorm`, `nnHolderNorm`	3
Theorems `exists_holderOnWith_of_le`, `exists_holderOnWith_of_le'`, `exists_holderOnWith_of_le_of_le`, `eHolderNorm_le`, `memHolder`, `nnholderNorm_le`, `add`, `coe_nnHolderNorm_eq_eHolderNorm`, `comp`, `eHolderNorm_lt_top`, `eHolderNorm_ne_top`, `holderWith`, `memHolder_of_le_of_le`, `nnHolderNorm_add_le`, `nnHolderNorm_eq_zero`, `nnHolderNorm_nsmul`, `nnHolderNorm_smul`, `nsmul`, `of_le`, `of_le'`, `smul`, `smul_iff`, `coe_nnHolderNorm_le_eHolderNorm`, `eHolderNorm_add_le`, `eHolderNorm_const`, `eHolderNorm_eq_top`, `eHolderNorm_eq_zero`, `eHolderNorm_lt_top`, `eHolderNorm_ne_top`, `eHolderNorm_nsmul`, `eHolderNorm_of_isEmpty`, `eHolderNorm_smul`, `eHolderNorm_zero`, `memHolder_const`, `memHolder_const'`, `memHolder_iff_holderWith`, `memHolder_zero`, `nnHolderNorm_const`, `nnHolderNorm_zero`	39
Total	42

HolderOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_holderOnWith_of_le` 📖	—	`HolderOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	—	—	`boundedSpace_val_set_iff` `MemHolder.of_le`
`exists_holderOnWith_of_le'` 📖	—	`HolderOnWith` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `ENNReal` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.ofNNReal`	—	—	`ne_top_of_le_ne_top` `ENNReal.coe_ne_top` `Metric.boundedSpace_iff_edist` `MemHolder.of_le`
`exists_holderOnWith_of_le_of_le` 📖	—	`HolderOnWith` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	—	—	`of_le_of_le`

HolderWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eHolderNorm_le` 📖	mathematical	`HolderWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eHolderNorm` `ENNReal.ofNNReal`	—	`iInf₂_le`
`memHolder` 📖	mathematical	`HolderWith`	`MemHolder`	—	—
`nnholderNorm_le` 📖	mathematical	`HolderWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `nnHolderNorm`	—	`ENNReal.coe_le_coe` `MemHolder.coe_nnHolderNorm_eq_eHolderNorm` `memHolder` `eHolderNorm_le`

MemHolder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`HolderWith.memHolder` `HolderWith.add` `holderWith`
`coe_nnHolderNorm_eq_eHolderNorm` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`ENNReal.ofNNReal` `nnHolderNorm` `eHolderNorm`	—	`nnHolderNorm.eq_1` `ENNReal.coe_toNNReal` `ne_of_lt` `lt_of_le_of_lt` `HolderWith.eHolderNorm_le` `holderWith` `ENNReal.coe_lt_top`
`comp` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`HolderWith.memHolder` `HolderWith.comp` `holderWith`
`eHolderNorm_lt_top` 📖	mathematical	`MemHolder`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eHolderNorm` `Top.top` `instTopENNReal`	—	`eHolderNorm_lt_top`
`eHolderNorm_ne_top` 📖	—	`MemHolder`	—	—	`eHolderNorm_ne_top`
`holderWith` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`HolderWith` `nnHolderNorm`	—	`PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd` `nnHolderNorm.eq_1` `eHolderNorm.eq_1` `ENNReal.coe_toNNReal` `LT.lt.ne` `eHolderNorm_lt_top` `ne_of_lt` `ENNReal.rpow_pos` `edist_pos` `edist_lt_top` `ENNReal.div_le_iff` `le_iInf₂`
`memHolder_of_le_of_le` 📖	—	`MemHolder` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	—	—	`HolderOnWith.exists_holderOnWith_of_le_of_le`
`nnHolderNorm_add_le` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `nnHolderNorm` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`LE.le.trans` `HolderWith.nnholderNorm_le` `holderWith` `add` `HolderWith.add`
`nnHolderNorm_eq_zero` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`nnHolderNorm` `NNReal` `instZeroNNReal`	—	`ENNReal.coe_eq_zero` `coe_nnHolderNorm_eq_eHolderNorm` `eHolderNorm_eq_zero`
`nnHolderNorm_nsmul` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`nnHolderNorm` `AddMonoid.toNatSMul` `Pi.addMonoid` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NNReal` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`Nat.cast_smul_eq_nsmul` `nnHolderNorm_smul` `NormedSpace.toNormSMulClass` `Real.nnnorm_natCast` `nsmul_eq_mul`
`nnHolderNorm_smul` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`nnHolderNorm` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing`	—	`ENNReal.coe_mul` `coe_nnHolderNorm_eq_eHolderNorm` `smul` `NormSMulClass.toIsBoundedSMul` `eHolderNorm_smul`
`nsmul` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`AddMonoid.toNatSMul` `Pi.addMonoid` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Nat.cast_smul_eq_nsmul` `smul` `NormedSpace.toIsBoundedSMul`
`of_le` 📖	—	`MemHolder` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	—	—	`Metric.boundedSpace_iff_edist` `holderOnWith_univ` `HolderOnWith.of_le`
`of_le'` 📖	—	`MemHolder` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `ENNReal` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.ofNNReal`	—	—	`ne_top_of_le_ne_top` `ENNReal.coe_ne_top` `Metric.boundedSpace_iff_edist` `of_le`
`smul` 📖	mathematical	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`HolderWith.memHolder` `HolderWith.smul` `holderWith`
`smul_iff` 📖	mathematical	—	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`HolderWith.smul_iff` `inv_mul_cancel_right₀` `smul` `NormSMulClass.toIsBoundedSMul`

(root)

Definitions

Name	Category	Theorems
`MemHolder` 📖	MathDef	9 math math: `eHolderNorm_lt_top`, `memHolder_zero`, `eHolderNorm_eq_top`, `memHolder_iff_holderWith`, `HolderWith.memHolder`, `eHolderNorm_ne_top`, `memHolder_const`, `memHolder_const'`, `MemHolder.smul_iff`
`eHolderNorm` 📖	CompOp	13 math math: `eHolderNorm_eq_zero`, `MemHolder.coe_nnHolderNorm_eq_eHolderNorm`, `coe_nnHolderNorm_le_eHolderNorm`, `eHolderNorm_lt_top`, `eHolderNorm_eq_top`, `eHolderNorm_const`, `eHolderNorm_of_isEmpty`, `eHolderNorm_nsmul`, `eHolderNorm_zero`, `eHolderNorm_add_le`, `HolderWith.eHolderNorm_le`, `eHolderNorm_smul`, `MemHolder.eHolderNorm_lt_top`
`nnHolderNorm` 📖	CompOp	11 math math: `MemHolder.holderWith`, `MemHolder.coe_nnHolderNorm_eq_eHolderNorm`, `coe_nnHolderNorm_le_eHolderNorm`, `nnHolderNorm_zero`, `nnHolderNorm_const`, `memHolder_iff_holderWith`, `MemHolder.nnHolderNorm_nsmul`, `MemHolder.nnHolderNorm_smul`, `MemHolder.nnHolderNorm_add_le`, `HolderWith.nnholderNorm_le`, `MemHolder.nnHolderNorm_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_nnHolderNorm_le_eHolderNorm` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `nnHolderNorm` `eHolderNorm`	—	`ENNReal.coe_toNNReal_le_self`
`eHolderNorm_add_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eHolderNorm` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`MemHolder.coe_nnHolderNorm_eq_eHolderNorm` `MemHolder.add` `ENNReal.coe_add` `ENNReal.coe_le_coe` `MemHolder.nnHolderNorm_add_le` `eHolderNorm_eq_top` `top_add` `add_top`
`eHolderNorm_const` 📖	mathematical	—	`eHolderNorm` `ENNReal` `instZeroENNReal`	—	`eHolderNorm.eq_1` `ENNReal.bot_eq_zero` `iInf₂_eq_bot` `HolderWith.const`
`eHolderNorm_eq_top` 📖	mathematical	—	`eHolderNorm` `Top.top` `ENNReal` `instTopENNReal` `MemHolder`	—	`eHolderNorm_ne_top`
`eHolderNorm_eq_zero` 📖	mathematical	—	`eHolderNorm` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `ENNReal` `instZeroENNReal`	—	`edist_eq_zero` `nonpos_iff_eq_zero` `ENNReal.instCanonicallyOrderedAdd` `le_of_forall_gt` `iInf₂_eq_bot` `ENNReal.bot_eq_zero` `eHolderNorm.eq_1` `ENNReal.div_pos` `LT.lt.ne` `ENNReal.rpow_lt_top_of_nonneg` `NNReal.zero_le_coe` `edist_lt_top` `lt_of_le_of_lt` `ENNReal.mul_lt_of_lt_div` `isEmpty_or_nonempty` `eHolderNorm_of_isEmpty` `eHolderNorm_const`
`eHolderNorm_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eHolderNorm` `Top.top` `instTopENNReal` `MemHolder`	—	`iInf_lt_top` `ENNReal.coe_lt_top`
`eHolderNorm_ne_top` 📖	mathematical	—	`MemHolder`	—	`eHolderNorm_lt_top` `lt_top_iff_ne_top`
`eHolderNorm_nsmul` 📖	mathematical	—	`eHolderNorm` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `AddMonoid.toNatSMul` `Pi.addMonoid` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ENNReal` `ENNReal.instTopologicalSpace` `instENormedAddCommMonoidENNReal`	—	`Nat.cast_smul_eq_nsmul` `eHolderNorm_smul` `NormedSpace.toNormSMulClass` `Real.nnnorm_natCast` `nsmul_eq_mul`
`eHolderNorm_of_isEmpty` 📖	mathematical	—	`eHolderNorm` `ENNReal` `instZeroENNReal`	—	`eHolderNorm.eq_1` `ENNReal.bot_eq_zero` `iInf₂_eq_bot` `HolderWith.of_isEmpty`
`eHolderNorm_smul` 📖	mathematical	—	`eHolderNorm` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing`	—	`nnnorm_eq_zero` `zero_smul` `eHolderNorm_zero` `nnnorm_zero` `MulZeroClass.zero_mul` `le_antisymm` `LE.le.trans` `HolderWith.eHolderNorm_le` `HolderWith.smul` `NormSMulClass.toIsBoundedSMul` `MemHolder.holderWith` `ENNReal.coe_mul` `MemHolder.coe_nnHolderNorm_eq_eHolderNorm` `mul_comm` `le_refl` `ENNReal.mul_le_of_le_div'` `HolderWith.memHolder` `ENNReal.coe_div` `ENNReal.mul_div_right_comm` `ENNReal.le_div_iff_mul_le` `ENNReal.coe_ne_zero` `ENNReal.coe_ne_top` `smul_eq_mul` `ENNReal.smul_def` `edist_smul₀` `Pi.smul_apply` `MemHolder.smul` `eHolderNorm_eq_top` `ENNReal.mul_top` `MemHolder.smul_iff` `LT.lt.ne` `MemHolder.eHolderNorm_lt_top`
`eHolderNorm_zero` 📖	mathematical	—	`eHolderNorm` `Pi.instZero` `ENNReal` `instZeroENNReal`	—	`eHolderNorm_const`
`memHolder_const` 📖	mathematical	—	`MemHolder`	—	`HolderWith.memHolder` `HolderWith.const`
`memHolder_const'` 📖	mathematical	—	`MemHolder`	—	`memHolder_const`
`memHolder_iff_holderWith` 📖	mathematical	—	`MemHolder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `HolderWith` `nnHolderNorm`	—	`MemHolder.holderWith` `HolderWith.memHolder`
`memHolder_zero` 📖	mathematical	—	`MemHolder` `Pi.instZero`	—	`memHolder_const`
`nnHolderNorm_const` 📖	mathematical	—	`nnHolderNorm` `NNReal` `instZeroNNReal`	—	`le_antisymm` `ENNReal.coe_le_coe` `le_trans` `coe_nnHolderNorm_le_eHolderNorm` `eHolderNorm_const` `ENNReal.coe_zero` `le_refl` `zero_le` `NNReal.instCanonicallyOrderedAdd`
`nnHolderNorm_zero` 📖	mathematical	—	`nnHolderNorm` `Pi.instZero` `NNReal` `instZeroNNReal`	—	`nnHolderNorm_const`

---

← Back to Index