Holder

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

Statistics

Metric	Count
Definitions `HolderOnWith`, `HolderWith`	2
Theorems `comp`, `comp_holderWith`, `continuousOn`, `dist_le`, `dist_le_of_le`, `ediam_image_inter_le`, `ediam_image_inter_le_of_le`, `ediam_image_le`, `ediam_image_le_of_le`, `ediam_image_le_of_subset`, `ediam_image_le_of_subset_of_le`, `edist_le`, `edist_le_of_le`, `holderOnWith_zero_of_bounded`, `holderWith`, `interpolate`, `interpolate_const`, `mono`, `mono_const`, `nndist_le`, `nndist_le_of_le`, `of_le`, `of_le_of_le`, `uniformContinuousOn`, `add`, `comp`, `comp_holderOnWith`, `const`, `continuous`, `dist_le`, `dist_le_of_le`, `ediam_image_le`, `edist_le`, `edist_le_of_le`, `holderOnWith`, `holderWith_zero_of_bounded`, `interpolate`, `interpolate_const`, `mono`, `nndist_le`, `nndist_le_of_le`, `of_isEmpty`, `of_le`, `of_le_of_le`, `restrict_iff`, `smul`, `smul_iff`, `uniformContinuous`, `zero`, `holderOnWith`, `holderWith`, `holderOnWith`, `convex_setOf_holderOnWith`, `convex_setOf_holderWith`, `holderOnWith_empty`, `holderOnWith_one`, `holderOnWith_singleton`, `holderOnWith_univ`, `holderWith_id`, `holderWith_one`, `holderWith_zero_iff`	61
Total	63

HolderOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`HolderOnWith` `Set.MapsTo`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`ENNReal.coe_mul` `mul_comm` `NNReal.coe_mul` `ENNReal.rpow_mul` `mul_assoc` `ENNReal.coe_rpow_of_nonneg` `NNReal.coe_nonneg` `ENNReal.mul_rpow_of_nonneg` `edist_le_of_le` `edist_le`
`comp_holderWith` 📖	mathematical	`HolderOnWith` `HolderWith` `Set` `Set.instMembership`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`holderOnWith_univ` `comp` `HolderWith.holderOnWith`
`continuousOn` 📖	mathematical	`HolderOnWith` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`UniformContinuousOn.continuousOn` `uniformContinuousOn`
`dist_le` 📖	mathematical	`HolderOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal` `Real.instPow`	—	`dist_le_of_le` `le_rfl`
`dist_le_of_le` 📖	mathematical	`HolderOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`Real.instMul` `NNReal.toReal` `Real.instPow`	—	`CanLift.prf` `NNReal.canLift` `LE.le.trans` `dist_nonneg` `dist_nndist` `nndist_le_of_le`
`ediam_image_inter_le` 📖	mathematical	`HolderOnWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.image` `Set` `Set.instInter` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`ediam_image_inter_le_of_le` `le_rfl`
`ediam_image_inter_le_of_le` 📖	mathematical	`HolderOnWith` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam`	`Set.image` `Set` `Set.instInter` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`ediam_image_le_of_subset_of_le` `Set.inter_subset_right` `LE.le.trans` `Metric.ediam_mono` `Set.inter_subset_left`
`ediam_image_le` 📖	mathematical	`HolderOnWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.image` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`ediam_image_le_of_le` `le_rfl`
`ediam_image_le_of_le` 📖	mathematical	`HolderOnWith` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam`	`Set.image` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`Metric.ediam_image_le_iff` `edist_le_of_le` `LE.le.trans` `Metric.edist_le_ediam_of_mem`
`ediam_image_le_of_subset` 📖	mathematical	`HolderOnWith` `Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.image` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`ediam_image_le` `mono`
`ediam_image_le_of_subset_of_le` 📖	mathematical	`HolderOnWith` `Set` `Set.instHasSubset` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam`	`Set.image` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`ediam_image_le_of_le` `mono`
`edist_le` 📖	mathematical	`HolderOnWith` `Set` `Set.instMembership`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	—
`edist_le_of_le` 📖	mathematical	`HolderOnWith` `Set` `Set.instMembership` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`LE.le.trans` `edist_le` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.rpow_le_rpow` `NNReal.coe_nonneg`
`holderOnWith_zero_of_bounded` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.ofNNReal` `HolderOnWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal` `instZeroNNReal`	—	`ENNReal.rpow_zero` `mul_one` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.rpow_le_rpow` `NNReal.coe_nonneg` `ENNReal.coe_mul` `ENNReal.coe_rpow_of_nonneg`
`holderWith` 📖	mathematical	`HolderOnWith`	`HolderWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	`HolderWith.restrict_iff`
`interpolate` 📖	mathematical	`HolderOnWith` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOneNNReal`	`Distrib.toMul` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`ENNReal.rpow_one` `le_imp_le_of_le_of_le` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.rpow_le_rpow` `NNReal.coe_nonneg` `le_refl` `mul_le_mul_right` `ENNReal.mul_rpow_of_nonneg` `ENNReal.coe_rpow_of_nonneg` `ENNReal.rpow_add_of_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `ENNReal.rpow_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`interpolate_const` 📖	mathematical	`HolderOnWith` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOneNNReal`	`Distrib.toMul`	—	`NNReal.rpow_one` `interpolate`
`mono` 📖	—	`HolderOnWith` `Set` `Set.instHasSubset`	—	—	`edist_le`
`mono_const` 📖	—	`HolderOnWith` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	—	—	`le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.coe_le_coe_of_le`
`nndist_le` 📖	mathematical	`HolderOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`nndist_le_of_le` `le_rfl`
`nndist_le_of_le` 📖	mathematical	`HolderOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`ENNReal.coe_le_coe` `edist_nndist` `ENNReal.coe_mul` `ENNReal.coe_rpow_of_nonneg` `NNReal.coe_nonneg` `edist_le_of_le`
`of_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.ofNNReal` `HolderOnWith` `NNReal` `instPartialOrderNNReal`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `Real.instSub` `NNReal.toReal`	—	`eq_zero_or_pos` `NNReal.instCanonicallyOrderedAdd` `sub_zero` `holderOnWith_zero_of_bounded` `LT.lt.trans_le` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.nnreal_coe_pos` `NNReal.coe_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instZeroLEOneClass` `NNReal.coe_le_coe` `NNReal.eq` `add_sub_cancel` `MulZeroClass.zero_mul` `add_zero` `mul_div_cancel₀` `LT.lt.ne'` `NNReal.mul_rpow` `NNReal.coe_nonneg` `NNReal.rpow_one` `mul_sub` `mul_one` `interpolate`
`of_le_of_le` 📖	mathematical	`HolderOnWith` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	`NNReal.instMax`	—	`mono_const` `le_max_left` `le_max_right` `Convex.segment_subset` `convex_setOf_holderOnWith` `NNReal.Icc_subset_segment`
`uniformContinuousOn` 📖	mathematical	`HolderOnWith` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`UniformContinuousOn` `PseudoEMetricSpace.toUniformSpace`	—	`EMetric.uniformContinuousOn_iff` `ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos` `ENNReal.coe_ne_top` `Filter.HasBasis.mem_iff` `ENNReal.nhds_zero_basis` `gt_mem_nhds` `ENNReal.instOrderTopology` `LE.le.trans_lt` `edist_le`

HolderWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`HolderWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`le_imp_le_of_le_of_le` `edist_add_add_le` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `add_le_add_right` `add_mul` `Distrib.rightDistribClass`
`comp` 📖	mathematical	`HolderWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`HolderOnWith.comp_holderWith` `holderOnWith`
`comp_holderOnWith` 📖	mathematical	`HolderWith` `HolderOnWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`HolderOnWith.comp` `holderOnWith`
`const` 📖	mathematical	—	`HolderWith`	—	`PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd`
`continuous` 📖	mathematical	`HolderWith` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`UniformContinuous.continuous` `uniformContinuous`
`dist_le` 📖	mathematical	`HolderWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal` `Real.instPow`	—	`dist_le_of_le` `le_rfl`
`dist_le_of_le` 📖	mathematical	`HolderWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`Real.instMul` `NNReal.toReal` `Real.instPow`	—	`HolderOnWith.dist_le_of_le` `holderOnWith` `Set.mem_univ`
`ediam_image_le` 📖	mathematical	`HolderWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.image` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`Metric.ediam_image_le_iff` `edist_le_of_le` `Metric.edist_le_ediam_of_mem`
`edist_le` 📖	mathematical	`HolderWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	—
`edist_le_of_le` 📖	mathematical	`HolderWith` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Real` `ENNReal.instPowReal` `NNReal.toReal`	—	`HolderOnWith.edist_le_of_le` `holderOnWith`
`holderOnWith` 📖	mathematical	`HolderWith`	`HolderOnWith`	—	—
`holderWith_zero_of_bounded` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.ofNNReal` `HolderWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal` `instZeroNNReal`	—	`holderOnWith_univ` `HolderOnWith.holderOnWith_zero_of_bounded`
`interpolate` 📖	mathematical	`HolderWith` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOneNNReal`	`Distrib.toMul` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`holderOnWith_univ` `HolderOnWith.interpolate`
`interpolate_const` 📖	mathematical	`HolderWith` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOneNNReal`	`Distrib.toMul`	—	`holderOnWith_univ` `HolderOnWith.interpolate_const`
`mono` 📖	—	`HolderWith` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	—	—	`LE.le.trans` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.coe_le_coe_of_le`
`nndist_le` 📖	mathematical	`HolderWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`nndist_le_of_le` `le_rfl`
`nndist_le_of_le` 📖	mathematical	`HolderWith` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `NNReal.toReal`	—	`HolderOnWith.nndist_le_of_le` `holderOnWith` `Set.mem_univ`
`of_isEmpty` 📖	mathematical	—	`HolderWith`	—	—
`of_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.ofNNReal` `HolderWith` `NNReal` `instPartialOrderNNReal`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Real` `NNReal.instPowReal` `Real.instSub` `NNReal.toReal`	—	`holderOnWith_univ` `HolderOnWith.of_le`
`of_le_of_le` 📖	mathematical	`HolderWith` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	`NNReal.instMax`	—	`holderOnWith_univ` `HolderOnWith.of_le_of_le`
`restrict_iff` 📖	mathematical	—	`HolderWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `HolderOnWith`	—	—
`smul` 📖	mathematical	`HolderWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Function.hasSMul` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`LE.le.trans` `edist_smul_le` `ENNReal.coe_mul` `ENNReal.smul_def` `smul_eq_mul` `mul_comm` `mul_assoc` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`
`smul_iff` 📖	mathematical	—	`HolderWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `SeminormedRing.toNonUnitalSeminormedRing` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`edist_smul₀` `mul_comm` `mul_assoc` `ENNReal.mul_le_mul_iff_right` `ENNReal.coe_ne_zero` `ENNReal.coe_ne_top`
`uniformContinuous` 📖	mathematical	`HolderWith` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`UniformContinuous` `PseudoEMetricSpace.toUniformSpace`	—	`uniformContinuousOn_univ` `HolderOnWith.uniformContinuousOn` `holderOnWith`
`zero` 📖	mathematical	—	`HolderWith` `Pi.instZero`	—	`const`

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`holderOnWith` 📖	mathematical	`LipschitzOnWith`	`HolderOnWith` `NNReal` `instOneNNReal`	—	`holderOnWith_one`

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`holderWith` 📖	mathematical	`LipschitzWith`	`HolderWith` `NNReal` `instOneNNReal`	—	`holderWith_one`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`holderOnWith` 📖	mathematical	`Set.Subsingleton`	`HolderOnWith`	—	`induction_on` `holderOnWith_empty` `holderOnWith_singleton`

(root)

Definitions

Name	Category	Theorems
`HolderOnWith` 📖	MathDef	9 math math: `holderOnWith_univ`, `HolderWith.holderOnWith`, `holderOnWith_empty`, `HolderWith.restrict_iff`, `holderOnWith_singleton`, `holderOnWith_one`, `LipschitzOnWith.holderOnWith`, `convex_setOf_holderOnWith`, `Set.Subsingleton.holderOnWith`
`HolderWith` 📖	MathDef	14 math math: `HolderWith.zero`, `holderOnWith_univ`, `MemHolder.holderWith`, `LipschitzWith.holderWith`, `HolderOnWith.holderWith`, `holderWith_zero_iff`, `memHolder_iff_holderWith`, `HolderWith.restrict_iff`, `HolderWith.of_isEmpty`, `convex_setOf_holderWith`, `holderWith_id`, `HolderWith.const`, `holderWith_one`, `HolderWith.smul_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convex_setOf_holderOnWith` 📖	mathematical	—	`Convex` `NNReal` `instSemiringNNReal` `instPartialOrderNNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `Algebra.id` `setOf` `HolderOnWith`	—	`smul_eq_mul` `mul_comm` `HolderOnWith.interpolate_const`
`convex_setOf_holderWith` 📖	mathematical	—	`Convex` `NNReal` `instSemiringNNReal` `instPartialOrderNNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `Algebra.id` `setOf` `HolderWith`	—	`convex_setOf_holderOnWith`
`holderOnWith_empty` 📖	mathematical	—	`HolderOnWith` `Set` `Set.instEmptyCollection`	—	—
`holderOnWith_one` 📖	mathematical	—	`HolderOnWith` `NNReal` `instOneNNReal` `LipschitzOnWith`	—	`ENNReal.rpow_one`
`holderOnWith_singleton` 📖	mathematical	—	`HolderOnWith` `Set` `Set.instSingletonSet`	—	`PseudoEMetricSpace.edist_self` `zero_le` `ENNReal.instCanonicallyOrderedAdd`
`holderOnWith_univ` 📖	mathematical	—	`HolderOnWith` `Set.univ` `HolderWith`	—	—
`holderWith_id` 📖	mathematical	—	`HolderWith` `NNReal` `instOneNNReal`	—	`LipschitzWith.holderWith` `LipschitzWith.id`
`holderWith_one` 📖	mathematical	—	`HolderWith` `NNReal` `instOneNNReal` `LipschitzWith`	—	`holderOnWith_univ` `holderOnWith_one` `lipschitzOnWith_univ`
`holderWith_zero_iff` 📖	mathematical	—	`HolderWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NNReal` `instZeroNNReal`	—	`MulZeroClass.zero_mul` `ENNReal.instCanonicallyOrderedAdd` `PseudoEMetricSpace.edist_self`

---

← Back to Index