Lipschitz

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

Statistics

Metric	Count
Definitions `toLocallyBoundedMap`	1
Theorems `dist_le_mul`, `extend_pi`, `extend_real`, `iff_le_add_mul`, `isBounded_image2`, `le_add_mul`, `mk_one`, `of_dist_le'`, `of_dist_le_mul`, `of_le_add`, `of_le_add_mul`, `of_le_add_mul'`, `coe_toLocallyBoundedMap`, `comap_cobounded_le`, `const_max`, `const_min`, `diam_image_le`, `dist`, `dist_iterate_succ_le_geometric`, `dist_le_mul`, `dist_le_mul_of_le`, `dist_left`, `dist_lt_mul_of_lt`, `dist_right`, `iff_le_add_mul`, `isBounded_image`, `le_add_mul`, `mapsTo_ball`, `mapsTo_closedBall`, `max`, `max_const`, `min`, `min_const`, `mk_one`, `nndist_le`, `of_dist_le'`, `of_dist_le_mul`, `of_le_add`, `of_le_add_mul`, `of_le_add_mul'`, `projIcc`, `properSpace`, `const_max`, `const_min`, `max`, `max_const`, `min`, `min_const`, `lipschitzWith_toNNReal`, `lipschitzOnWith_iff_dist_le_mul`, `lipschitzWith_iff_dist_le_mul`, `lipschitzWith_max`, `lipschitzWith_min`	53
Total	54

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_le_mul` 📖	mathematical	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Set` `Set.instMembership`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	—	`lipschitzOnWith_iff_dist_le_mul`
`extend_pi` 📖	mathematical	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `pseudoEMetricSpacePi` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`LipschitzWith` `Set.EqOn`	—	`of_dist_le_mul` `LE.le.trans` `dist_le_pi_dist` `dist_le_mul` `extend_real` `LipschitzWith.of_dist_le_mul` `dist_pi_le_iff` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_nonneg` `LipschitzWith.dist_le_mul`
`extend_real` 📖	mathematical	`LipschitzOnWith` `Real` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`LipschitzWith` `Set.EqOn`	—	`Set.eq_empty_or_nonempty` `LipschitzWith.weaken` `LipschitzWith.const` `zero_le` `NNReal.instCanonicallyOrderedAdd` `Set.eqOn_empty` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_assoc` `mul_add` `Distrib.leftDistribClass` `add_comm` `le_add_mul` `add_le_add_right` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_triangle_left` `NNReal.coe_nonneg` `le_antisymm` `le_ciInf` `dist_self` `MulZeroClass.mul_zero` `add_zero` `ciInf_le` `LipschitzWith.of_le_add_mul` `dist_triangle`
`iff_le_add_mul` 📖	mathematical	—	`LipschitzOnWith` `Real` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Real.instLE` `Real.instAdd` `Real.instMul` `NNReal.toReal` `Dist.dist` `PseudoMetricSpace.toDist`	—	`le_add_mul` `of_le_add_mul`
`isBounded_image2` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.image2`	—	`Metric.isBounded_iff_ediam_ne_top` `ne_top_of_le_ne_top` `ENNReal.add_ne_top` `ENNReal.mul_ne_top` `ENNReal.coe_ne_top` `Bornology.IsBounded.ediam_ne_top` `ediam_image2_le`
`le_add_mul` 📖	mathematical	`LipschitzOnWith` `Real` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Set` `Set.instMembership`	`Real.instLE` `Real.instAdd` `Real.instMul` `NNReal.toReal` `Dist.dist` `PseudoMetricSpace.toDist`	—	`sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_trans` `le_abs_self` `dist_le_mul`
`mk_one` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal` `instOneNNReal`	—	`of_dist_le_mul` `one_mul`
`of_dist_le'` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Real.toNNReal`	—	`of_dist_le_mul` `le_trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Real.le_coe_toNNReal` `dist_nonneg`
`of_dist_le_mul` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`lipschitzOnWith_iff_dist_le_mul`
`of_le_add` 📖	mathematical	`Real` `Real.instLE` `Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist`	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOneNNReal`	—	`of_le_add_mul` `one_mul`
`of_le_add_mul` 📖	mathematical	`Real` `Real.instLE` `Real.instAdd` `Real.instMul` `NNReal.toReal` `Dist.dist` `PseudoMetricSpace.toDist`	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	—	`Real.toNNReal_coe` `of_le_add_mul'`
`of_le_add_mul'` 📖	mathematical	`Real` `Real.instLE` `Real.instAdd` `Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist`	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Real.toNNReal`	—	`sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `of_dist_le'` `abs_sub_le_iff` `dist_comm`

LipschitzWith

Definitions

Name	Category	Theorems
`toLocallyBoundedMap` 📖	CompOp	1 math math: `coe_toLocallyBoundedMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toLocallyBoundedMap` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`DFunLike.coe` `LocallyBoundedMap` `PseudoMetricSpace.toBornology` `LocallyBoundedMap.instFunLike` `toLocallyBoundedMap`	—	—
`comap_cobounded_le` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`LocallyBoundedMap.comap_cobounded_le'`
`const_max` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMax`	—	`max_comm` `max_const`
`const_min` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMin`	—	`min_comm` `min_const`
`diam_image_le` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`Real` `Real.instLE` `Metric.diam` `Set.image` `Real.instMul` `NNReal.toReal`	—	`Metric.diam_le_of_forall_dist_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `NNReal.coe_nonneg` `Metric.diam_nonneg` `Set.forall_mem_image` `dist_le_mul_of_le` `Metric.dist_le_diam_of_mem`
`dist` 📖	mathematical	—	`LipschitzWith` `Real` `Prod.pseudoEMetricSpaceMax` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Nat.instAtLeastTwoHAddOfNat` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Nat.instAtLeastTwoHAddOfNat` `one_add_one_eq_two` `uncurry` `dist_left` `dist_right`
`dist_iterate_succ_le_geometric` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Nat.iterate` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `NNReal.toReal`	—	`Function.iterate_succ` `mul_comm` `dist_le_mul` `iterate`
`dist_le_mul` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	—	`lipschitzWith_iff_dist_le_mul`
`dist_le_mul_of_le` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`Real.instMul` `NNReal.toReal`	—	`LE.le.trans` `dist_le_mul` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `NNReal.coe_nonneg`
`dist_left` 📖	mathematical	—	`LipschitzWith` `Real` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOneNNReal` `Dist.dist` `PseudoMetricSpace.toDist`	—	`mk_one` `dist_dist_dist_le_left`
`dist_lt_mul_of_lt` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLT` `Dist.dist` `PseudoMetricSpace.toDist`	`Real.instMul` `NNReal.toReal`	—	`LE.le.trans_lt` `dist_le_mul` `mul_lt_mul_of_pos_left` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd`
`dist_right` 📖	mathematical	—	`LipschitzWith` `Real` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOneNNReal` `Dist.dist` `PseudoMetricSpace.toDist`	—	`of_le_add` `dist_triangle_right`
`iff_le_add_mul` 📖	mathematical	—	`LipschitzWith` `Real` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Real.instLE` `Real.instAdd` `Real.instMul` `NNReal.toReal` `Dist.dist` `PseudoMetricSpace.toDist`	—	`le_add_mul` `of_le_add_mul`
`isBounded_image` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`Set.image`	—	`Bornology.IsBounded.image` `LocallyBoundedMap.instLocallyBoundedMapClass`
`le_add_mul` 📖	mathematical	`LipschitzWith` `Real` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instLE` `Real.instAdd` `Real.instMul` `NNReal.toReal` `Dist.dist` `PseudoMetricSpace.toDist`	—	`sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_trans` `le_abs_self` `dist_le_mul`
`mapsTo_ball` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.MapsTo` `Metric.ball` `Real` `Real.instMul` `NNReal.toReal`	—	`dist_lt_mul_of_lt`
`mapsTo_closedBall` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Set.MapsTo` `Metric.closedBall` `Real` `Real.instMul` `NNReal.toReal`	—	`dist_le_mul_of_le`
`max` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`NNReal` `NNReal.instMax` `Real.instMax`	—	`one_mul` `comp` `lipschitzWith_max` `prodMk`
`max_const` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMax`	—	`max_eq_left` `zero_le` `NNReal.instCanonicallyOrderedAdd` `max` `const`
`min` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`NNReal` `NNReal.instMax` `Real.instMin`	—	`one_mul` `comp` `lipschitzWith_min` `prodMk`
`min_const` 📖	mathematical	`LipschitzWith` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMin`	—	`max_eq_left` `zero_le` `NNReal.instCanonicallyOrderedAdd` `min` `const`
`mk_one` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist`	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal` `instOneNNReal`	—	`of_dist_le_mul` `one_mul`
`nndist_le` 📖	mathematical	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`dist_le_mul`
`of_dist_le'` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul`	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Real.toNNReal`	—	`of_dist_le_mul` `le_trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Real.le_coe_toNNReal` `dist_nonneg`
`of_dist_le_mul` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`lipschitzWith_iff_dist_le_mul`
`of_le_add` 📖	mathematical	`Real` `Real.instLE` `Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist`	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOneNNReal`	—	`of_le_add_mul` `one_mul`
`of_le_add_mul` 📖	mathematical	`Real` `Real.instLE` `Real.instAdd` `Real.instMul` `NNReal.toReal` `Dist.dist` `PseudoMetricSpace.toDist`	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	—	`Real.toNNReal_coe` `of_le_add_mul'`
`of_le_add_mul'` 📖	mathematical	`Real` `Real.instLE` `Real.instAdd` `Real.instMul` `Dist.dist` `PseudoMetricSpace.toDist`	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `Real.toNNReal`	—	`sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `of_dist_le'` `abs_sub_le_iff` `dist_comm`
`projIcc` 📖	mathematical	`Real` `Real.instLE`	`LipschitzWith` `Set.Elem` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.linearOrder` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `NNReal` `instOneNNReal` `Set.projIcc`	—	`const_max` `const_min` `id`
`properSpace` 📖	mathematical	`IsProperMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`ProperSpace`	—	`IsCompact.of_isClosed_subset` `IsProperMap.isCompact_preimage` `ProperSpace.isCompact_closedBall` `Metric.isClosed_closedBall` `Set.MapsTo.subset_preimage` `mapsTo_closedBall`

LocallyLipschitz

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_max` 📖	mathematical	`LocallyLipschitz` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMax`	—	`max_comm` `max_const`
`const_min` 📖	mathematical	`LocallyLipschitz` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMin`	—	`min_comm` `min_const`
`max` 📖	mathematical	`LocallyLipschitz` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMax`	—	`comp` `LipschitzWith.locallyLipschitz` `lipschitzWith_max` `prodMk`
`max_const` 📖	mathematical	`LocallyLipschitz` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMax`	—	`max` `const`
`min` 📖	mathematical	`LocallyLipschitz` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMin`	—	`comp` `LipschitzWith.locallyLipschitz` `lipschitzWith_min` `prodMk`
`min_const` 📖	mathematical	`LocallyLipschitz` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace`	`Real.instMin`	—	`min` `const`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lipschitzWith_toNNReal` 📖	mathematical	—	`LipschitzWith` `Real` `NNReal` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `instMetricSpaceNNReal` `instOneNNReal` `toNNReal`	—	`lipschitzWith_iff_dist_le_mul` `one_mul` `dist_prod_same_right` `lipschitzWith_max`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lipschitzOnWith_iff_dist_le_mul` 📖	mathematical	—	`LipschitzOnWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	—	`edist_nndist`
`lipschitzWith_iff_dist_le_mul` 📖	mathematical	—	`LipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	—	`edist_nndist`
`lipschitzWith_max` 📖	mathematical	—	`LipschitzWith` `Real` `Prod.pseudoEMetricSpaceMax` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOneNNReal` `Real.instMax`	—	`LipschitzWith.of_le_add` `sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans` `le_abs_self` `abs_max_sub_max_le_max`
`lipschitzWith_min` 📖	mathematical	—	`LipschitzWith` `Real` `Prod.pseudoEMetricSpaceMax` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `instOneNNReal` `Real.instMin`	—	`LipschitzWith.of_le_add` `sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LE.le.trans` `le_abs_self` `abs_min_sub_min_le_max`

---

← Back to Index