Documentation Verification Report

ContinuousFunctions

📁 Source: Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean

Statistics

Metric	Count
Definitions `toLp`, `toLpHom`, `toLp`, `boundedContinuousFunction`	4
Theorems `Lp_nnnorm_le`, `Lp_norm_le`, `coeFn_toLp`, `memLp_top`, `mem_Lp`, `range_toLp`, `range_toLpHom`, `toLp_inj`, `toLp_injective`, `toLp_norm_le`, `coeFn_toLp`, `coe_toLp`, `hasSum_of_hasSum_Lp`, `range_toLp`, `toLp_comp_toContinuousMap`, `toLp_def`, `toLp_inj`, `toLp_injective`, `toLp_norm_eq_toLp_norm_coe`, `toLp_norm_le`, `mem_boundedContinuousFunction_iff`	21
Total	25

BoundedContinuousFunction

Definitions

Name	Category	Theorems
`toLp` 📖	CompOp	10 math math: `toLp_inj`, `toLp_injective`, `ContinuousMap.toLp_def`, `ContinuousMap.toLp_norm_eq_toLp_norm_coe`, `coeFn_toLp`, `ContinuousMap.toLp_comp_toContinuousMap`, `toLp_norm_le`, `MeasureTheory.BoundedContinuousFunction.inner_toLp`, `range_toLp`, `toLp_denseRange`
`toLpHom` 📖	CompOp	1 math math: `range_toLpHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Lp_nnnorm_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `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` `ContinuousMap.toAEEqFun` `PseudoEMetricSpace.pseudoMetrizableSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `toContinuousMap` `mem_Lp` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `MeasureTheory.measureUnivNNReal` `Real.instInv` `ENNReal.toReal` `BoundedContinuousFunction` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `instSeminormedAddCommGroup`	—	`MeasureTheory.Lp.nnnorm_le_of_ae_bound` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `PseudoEMetricSpace.pseudoMetrizableSpace` `mem_Lp` `Filter.Eventually.mono` `MeasureTheory.Measure.instOuterMeasureClass` `ContinuousMap.coeFn_toAEEqFun` `NNReal.coe_le_coe` `coe_nnnorm` `norm_coe_le_norm`
`Lp_norm_le` 📖	mathematical	—	`Real` `Real.instLE` `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` `ContinuousMap.toAEEqFun` `PseudoEMetricSpace.pseudoMetrizableSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `toContinuousMap` `mem_Lp` `Real.instMul` `Real.instPow` `NNReal.toReal` `MeasureTheory.measureUnivNNReal` `Real.instInv` `ENNReal.toReal` `BoundedContinuousFunction` `instNorm`	—	`Lp_nnnorm_le`
`coeFn_toLp` 📖	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` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `BoundedContinuousFunction` `instPseudoMetricSpace` `instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Lp.instNormedAddCommGroup` `instModule` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp` `instFunLike`	—	—
`memLp_top` 📖	mathematical	—	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `BoundedContinuousFunction` `instFunLike` `Top.top` `ENNReal` `instTopENNReal`	—	`Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ContinuousMapClass.map_continuous` `BoundedContinuousMapClass.toContinuousMapClass` `instBoundedContinuousMapClass` `MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `norm_coe_le_norm`
`mem_Lp` 📖	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` `ContinuousMap.toAEEqFun` `PseudoEMetricSpace.pseudoMetrizableSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `toContinuousMap`	—	`MeasureTheory.Lp.mem_Lp_of_ae_bound` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `ContinuousMap.coeFn_toAEEqFun` `Filter.univ_mem'` `norm_coe_le_norm`
`range_toLp` 📖	mathematical	—	`Submodule.toAddSubgroup` `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` `NormedRing.toRing` `AddSubgroup.toAddCommGroup` `MeasureTheory.AEEqFun.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `LinearMap.range` `BoundedContinuousFunction` `Ring.toSemiring` `instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Lp.instNormedAddCommGroup` `instModule` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `instPseudoMetricSpace` `toLp` `MeasureTheory.Lp.boundedContinuousFunction`	—	`range_toLpHom`
`range_toLpHom` 📖	mathematical	—	`NormedAddGroupHom.range` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instSeminormedAddCommGroup` `MeasureTheory.Lp.instNormedAddCommGroup` `toLpHom` `MeasureTheory.Lp.boundedContinuousFunction`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `AddMonoidHom.addSubgroupOf_range_eq_of_le` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `mem_Lp`
`toLp_inj` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNormedAddCommGroup` `instModule` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `DFunLike.coe_fn_eq` `MeasureTheory.Measure.instOuterMeasureClass` `Continuous.ae_eq_iff_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ContinuousMapClass.map_continuous` `BoundedContinuousMapClass.toContinuousMapClass` `instBoundedContinuousMapClass` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.symm` `coeFn_toLp` `Filter.EventuallyEq.refl`
`toLp_injective` 📖	mathematical	—	`BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `instPseudoMetricSpace` `instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Lp.instNormedAddCommGroup` `instModule` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd`
`toLp_norm_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpace` `instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNormedAddCommGroup` `instModule` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedSpace.toModule` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.hasOpNorm` `instSeminormedAddCommGroup` `instNormedSpace` `MeasureTheory.Lp.instNormedSpace` `toLp` `Real.instPow` `NNReal.toReal` `MeasureTheory.measureUnivNNReal` `Real.instInv` `ENNReal.toReal`	—	`LinearMap.mkContinuous_norm_le` `NormedSpace.toIsBoundedSMul` `mem_Lp` `NNReal.coe_nonneg` `Lp_norm_le`

ContinuousMap

Definitions

Name	Category	Theorems
`toLp` 📖	CompOp	13 math math: `toLp_inj`, `toLp_denseRange`, `range_toLp`, `toLp_norm_le`, `UnitAddTorus.mFourierCoeff_toLp`, `toLp_def`, `toLp_norm_eq_toLp_norm_coe`, `fourierCoeff_toLp`, `toLp_injective`, `coe_toLp`, `coeFn_toLp`, `toLp_comp_toContinuousMap`, `MeasureTheory.ContinuousMap.inner_toLp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_toLp` 📖	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` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `compactOpen` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp` `instFunLike`	—	—
`coe_toLp` 📖	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` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `compactOpen` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp` `toAEEqFun` `PseudoEMetricSpace.pseudoMetrizableSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul`
`hasSum_of_hasSum_Lp` 📖	—	`Summable` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `compactOpen` `SummationFilter.unconditional` `HasSum` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp`	—	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `toLp_injective` `HasSum.unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `ContinuousLinearMap.hasSum` `Summable.hasSum`
`range_toLp` 📖	mathematical	—	`Submodule.toAddSubgroup` `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` `NormedRing.toRing` `AddSubgroup.toAddCommGroup` `MeasureTheory.AEEqFun.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `LinearMap.range` `ContinuousMap` `Ring.toSemiring` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `compactOpen` `toLp` `MeasureTheory.Lp.boundedContinuousFunction`	—	`SetLike.ext'` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `RingHomSurjective.ids` `RingHomInvPair.ids` `LinearIsometryEquiv.surjective` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `BoundedContinuousFunction.range_toLp` `Submodule.coe_toAddSubgroup` `LinearMap.coe_range` `ContinuousLinearMap.coe_coe` `Function.Surjective.range_comp`
`toLp_comp_toContinuousMap` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `compactOpen` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp` `BoundedContinuousFunction.toContinuousMap` `BoundedContinuousFunction` `BoundedContinuousFunction.instPseudoMetricSpace` `BoundedContinuousFunction.instAddCommMonoid` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `BoundedContinuousFunction.instModule` `BoundedContinuousFunction.toLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul`
`toLp_def` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `compactOpen` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp` `BoundedContinuousFunction` `BoundedContinuousFunction.instPseudoMetricSpace` `BoundedContinuousFunction.instAddCommMonoid` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `BoundedContinuousFunction.instModule` `BoundedContinuousFunction.toLp` `LinearIsometryEquiv` `RingHomInvPair.ids` `instSeminormedAddCommGroup` `BoundedContinuousFunction.instSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `linearIsometryBoundedOfCompact`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul`
`toLp_inj` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `compactOpen` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `toLp_injective`
`toLp_injective` 📖	mathematical	—	`ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `compactOpen` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.funLike` `toLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsTopologicalAddGroup.toContinuousAdd` `BoundedContinuousFunction.toLp_injective` `LinearIsometryEquiv.injective` `RingHomInvPair.ids` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul`
`toLp_norm_eq_toLp_norm_coe` 📖	mathematical	—	`Norm.norm` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `compactOpen` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `NormedSpace.toModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.hasOpNorm` `instSeminormedAddCommGroup` `normedSpace` `MeasureTheory.Lp.instNormedSpace` `toLp` `BoundedContinuousFunction` `BoundedContinuousFunction.instPseudoMetricSpace` `BoundedContinuousFunction.instAddCommMonoid` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `BoundedContinuousFunction.instModule` `BoundedContinuousFunction.instSeminormedAddCommGroup` `BoundedContinuousFunction.instNormedSpace` `BoundedContinuousFunction.toLp`	—	`ContinuousLinearMap.opNorm_comp_linearIsometryEquiv` `RingHomCompTriple.ids` `RingHomIsometric.ids` `NormedSpace.toIsBoundedSMul`
`toLp_norm_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `compactOpen` `instAddCommMonoidOfContinuousAdd` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.AEEqFun` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `MeasureTheory.Lp.instNormedAddCommGroup` `module` `NormedSpace.toModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `MeasureTheory.Lp.instModule` `ContinuousLinearMap.hasOpNorm` `instSeminormedAddCommGroup` `normedSpace` `MeasureTheory.Lp.instNormedSpace` `toLp` `Real.instPow` `NNReal.toReal` `MeasureTheory.measureUnivNNReal` `Real.instInv` `ENNReal.toReal`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `toLp_norm_eq_toLp_norm_coe` `BoundedContinuousFunction.toLp_norm_le`

MeasureTheory.Lp

Definitions

Name	Category	Theorems
`boundedContinuousFunction` 📖	CompOp	6 math math: `ContinuousMap.range_toLp`, `boundedContinuousFunction_topologicalClosure`, `BoundedContinuousFunction.range_toLpHom`, `boundedContinuousFunction_dense`, `mem_boundedContinuousFunction_iff`, `BoundedContinuousFunction.range_toLp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_boundedContinuousFunction_iff` 📖	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` `AddSubgroup.toAddGroup` `boundedContinuousFunction` `ContinuousMap.toAEEqFun` `PseudoEMetricSpace.pseudoMetrizableSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `BoundedContinuousFunction.toContinuousMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `AddSubgroup.mem_addSubgroupOf`

---

← Back to Index