Lipschitz

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

Statistics

Metric	Count
Definitions `LipschitzOnWith`, `LipschitzWith`, `LocallyLipschitz`, `LocallyLipschitzOn`	4
Theorems `comp`, `continuousOn`, `ediam_image2_le`, `edist_le_mul_of_le`, `edist_lt_of_edist_lt_div`, `mapsToRestrict`, `mono`, `prodMk`, `to_restric_mapsTo`, `to_restrict`, `uniformContinuousOn`, `zero_iff`, `comp`, `comp_lipschitzOnWith`, `const`, `const'`, `continuous`, `ediam_image_le`, `edist_iterate_succ_le_geometric`, `edist_le_mul`, `edist_le_mul_of_le`, `edist_lt_mul_of_lt`, `edist_lt_of_edist_lt_div`, `edist_lt_top`, `eval`, `id`, `iterate`, `lipschitzOnWith`, `list_prod`, `locallyLipschitz`, `mapsTo_closedEBall`, `mapsTo_eball`, `mapsTo_emetric_ball`, `mapsTo_emetric_closedBall`, `mul_edist_le`, `mul_end`, `of_edist_le`, `pow_end`, `prodMk`, `prodMk_left`, `prodMk_right`, `prod_fst`, `prod_snd`, `restrict`, `subtype_mk`, `subtype_val`, `uncurry`, `uniformContinuous`, `weaken`, `zero_iff`, `comp`, `const`, `continuous`, `id`, `iterate`, `locallyLipschitzOn`, `mul_end`, `pow_end`, `prodMk`, `prodMk_left`, `prodMk_right`, `continuousOn`, `mono`, `restrict`, `lipschitzOnWith_iff_restrict`, `continuousOn_prod_of_continuousOn_lipschitzOnWith`, `continuousOn_prod_of_continuousOn_lipschitzOnWith'`, `continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith`, `continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith'`, `continuous_prod_of_continuous_lipschitzWith`, `continuous_prod_of_continuous_lipschitzWith'`, `continuous_prod_of_dense_continuous_lipschitzWith`, `continuous_prod_of_dense_continuous_lipschitzWith'`, `lipschitzOnWith_empty`, `lipschitzOnWith_iff_restrict`, `lipschitzOnWith_restrict`, `lipschitzOnWith_univ`, `locallyLipschitzOn_empty`, `locallyLipschitzOn_iff_restrict`, `locallyLipschitzOn_univ`	80
Total	84

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`LipschitzOnWith` `Set.MapsTo`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`lipschitzOnWith_iff_restrict` `LipschitzWith.comp` `to_restrict` `mapsToRestrict`
`continuousOn` 📖	mathematical	`LipschitzOnWith`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`UniformContinuousOn.continuousOn` `uniformContinuousOn`
`ediam_image2_le` 📖	mathematical	`LipschitzOnWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.image2` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Distrib.toMul` `ENNReal.ofNNReal`	—	`LE.le.trans` `PseudoEMetricSpace.edist_triangle` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mul_right_mono` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `Metric.edist_le_ediam_of_mem`
`edist_le_mul_of_le` 📖	mathematical	`LipschitzOnWith` `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`	—	`LE.le.trans` `mul_right_mono` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`
`edist_lt_of_edist_lt_div` 📖	—	`LipschitzOnWith` `Set` `Set.instMembership` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `ENNReal.ofNNReal`	—	—	`LipschitzWith.edist_lt_of_edist_lt_div` `to_restrict`
`mapsToRestrict` 📖	mathematical	`Set.MapsTo` `LipschitzOnWith`	`LipschitzWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.MapsTo.restrict`	—	`Set.MapsTo.lipschitzOnWith_iff_restrict`
`mono` 📖	—	`LipschitzOnWith` `Set` `Set.instHasSubset`	—	—	—
`prodMk` 📖	mathematical	`LipschitzOnWith`	`Prod.pseudoEMetricSpaceMax` `NNReal` `NNReal.instMax`	—	`Monotone.map_max` `ENNReal.coe_mono` `Prod.edist_eq` `max_mul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `max_le_max`
`to_restric_mapsTo` 📖	mathematical	`Set.MapsTo` `LipschitzOnWith`	`LipschitzWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.MapsTo.restrict`	—	`mapsToRestrict`
`to_restrict` 📖	mathematical	`LipschitzOnWith`	`LipschitzWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	`lipschitzOnWith_iff_restrict`
`uniformContinuousOn` 📖	mathematical	`LipschitzOnWith`	`UniformContinuousOn` `PseudoEMetricSpace.toUniformSpace`	—	`uniformContinuousOn_iff_restrict` `LipschitzWith.uniformContinuous` `to_restrict`
`zero_iff` 📖	mathematical	—	`LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `instZeroNNReal`	—	`MulZeroClass.zero_mul` `ENNReal.instCanonicallyOrderedAdd`

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`LipschitzWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`mul_right_mono` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `mul_assoc` `ENNReal.coe_mul`
`comp_lipschitzOnWith` 📖	mathematical	`LipschitzWith` `LipschitzOnWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`lipschitzOnWith_iff_restrict` `comp` `LipschitzOnWith.to_restrict`
`const` 📖	mathematical	—	`LipschitzWith` `NNReal` `instZeroNNReal`	—	`PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd`
`const'` 📖	mathematical	—	`LipschitzWith`	—	`PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd`
`continuous` 📖	mathematical	`LipschitzWith`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`UniformContinuous.continuous` `uniformContinuous`
`ediam_image_le` 📖	mathematical	`LipschitzWith`	`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`	—	`Metric.ediam_le` `edist_le_mul_of_le` `Metric.edist_le_ediam_of_mem`
`edist_iterate_succ_le_geometric` 📖	mathematical	`LipschitzWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Nat.iterate` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `ENNReal.ofNNReal`	—	`Function.iterate_succ` `mul_comm` `iterate`
`edist_le_mul` 📖	mathematical	`LipschitzWith`	`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`	—	—
`edist_le_mul_of_le` 📖	mathematical	`LipschitzWith` `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`	—	`LE.le.trans` `mul_right_mono` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`
`edist_lt_mul_of_lt` 📖	mathematical	`LipschitzWith` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`lt_imp_lt_of_le_of_le` `le_refl` `ENNReal.mul_lt_mul_right` `ne_of_gt` `ENNReal.coe_pos` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd`
`edist_lt_of_edist_lt_div` 📖	—	`LipschitzWith` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `ENNReal.ofNNReal`	—	—	`ENNReal.mul_lt_of_lt_div'`
`edist_lt_top` 📖	mathematical	`LipschitzWith`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Top.top` `instTopENNReal`	—	`LE.le.trans_lt` `Ne.lt_top` `ENNReal.mul_ne_top` `ENNReal.coe_ne_top`
`eval` 📖	mathematical	—	`LipschitzWith` `pseudoEMetricSpacePi` `NNReal` `instOneNNReal` `Function.eval`	—	`of_edist_le` `edist_le_pi_edist`
`id` 📖	mathematical	—	`LipschitzWith` `NNReal` `instOneNNReal`	—	`of_edist_le` `le_rfl`
`iterate` 📖	mathematical	`LipschitzWith`	`NNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `Nat.iterate`	—	`pow_zero` `id` `pow_succ` `comp`
`lipschitzOnWith` 📖	mathematical	`LipschitzWith`	`LipschitzOnWith`	—	—
`list_prod` 📖	mathematical	`LipschitzWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOneNNReal` `Function.End` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoidEnd` `MulOne.toOne`	—	`id` `mul_end`
`locallyLipschitz` 📖	mathematical	`LipschitzWith`	`LocallyLipschitz`	—	`Filter.univ_mem` `lipschitzOnWith_univ`
`mapsTo_closedEBall` 📖	mathematical	`LipschitzWith`	`Set.MapsTo` `Metric.closedEBall` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`edist_le_mul_of_le`
`mapsTo_eball` 📖	mathematical	`LipschitzWith`	`Set.MapsTo` `Metric.eball` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`edist_lt_mul_of_lt`
`mapsTo_emetric_ball` 📖	mathematical	`LipschitzWith`	`Set.MapsTo` `Metric.eball` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`mapsTo_eball`
`mapsTo_emetric_closedBall` 📖	mathematical	`LipschitzWith`	`Set.MapsTo` `Metric.closedEBall` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`mapsTo_closedEBall`
`mul_edist_le` 📖	mathematical	`LipschitzWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv` `ENNReal.ofNNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`mul_comm` `div_eq_mul_inv` `ENNReal.div_le_of_le_mul'`
`mul_end` 📖	mathematical	`LipschitzWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Function.End` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoidEnd`	—	`comp`
`of_edist_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist`	`LipschitzWith` `NNReal` `instOneNNReal`	—	`one_mul`
`pow_end` 📖	mathematical	`LipschitzWith`	`NNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `Function.End` `instMonoidEnd`	—	`pow_zero` `id` `pow_succ` `mul_end`
`prodMk` 📖	mathematical	`LipschitzWith`	`Prod.pseudoEMetricSpaceMax` `NNReal` `NNReal.instMax`	—	`Monotone.map_max` `ENNReal.coe_mono` `Prod.edist_eq` `max_mul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `max_le_max`
`prodMk_left` 📖	mathematical	—	`LipschitzWith` `Prod.pseudoEMetricSpaceMax` `NNReal` `instOneNNReal`	—	`max_eq_right` `zero_le_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `prodMk` `const` `id`
`prodMk_right` 📖	mathematical	—	`LipschitzWith` `Prod.pseudoEMetricSpaceMax` `NNReal` `instOneNNReal`	—	`max_eq_left` `zero_le_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `prodMk` `id` `const`
`prod_fst` 📖	mathematical	—	`LipschitzWith` `Prod.pseudoEMetricSpaceMax` `NNReal` `instOneNNReal`	—	`of_edist_le` `le_max_left`
`prod_snd` 📖	mathematical	—	`LipschitzWith` `Prod.pseudoEMetricSpaceMax` `NNReal` `instOneNNReal`	—	`of_edist_le` `le_max_right`
`restrict` 📖	mathematical	`LipschitzWith`	`Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	—
`subtype_mk` 📖	mathematical	`LipschitzWith`	`instPseudoEMetricSpaceSubtype`	—	—
`subtype_val` 📖	mathematical	—	`LipschitzWith` `Set` `Set.instMembership` `instPseudoEMetricSpaceSubtype` `NNReal` `instOneNNReal`	—	`of_edist_le` `le_rfl`
`uncurry` 📖	mathematical	`LipschitzWith`	`Prod.pseudoEMetricSpaceMax` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`add_mul` `Distrib.rightDistribClass` `le_trans` `PseudoEMetricSpace.edist_triangle` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mul_right_mono` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `le_max_left` `le_max_right`
`uniformContinuous` 📖	mathematical	`LipschitzWith`	`UniformContinuous` `PseudoEMetricSpace.toUniformSpace`	—	`EMetric.uniformContinuous_iff` `ENNReal.div_pos_iff` `ne_of_gt` `ENNReal.coe_ne_top` `edist_lt_of_edist_lt_div`
`weaken` 📖	—	`LipschitzWith` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal`	—	—	`le_trans` `mul_left_mono` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.coe_le_coe`
`zero_iff` 📖	mathematical	—	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `instZeroNNReal`	—	`MulZeroClass.zero_mul` `ENNReal.instCanonicallyOrderedAdd`

LocallyLipschitz

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`LocallyLipschitz`	—	—	`Filter.inter_mem` `Continuous.continuousAt` `continuous` `LipschitzOnWith.comp` `LipschitzOnWith.mono` `Set.inter_subset_left` `Set.MapsTo.mono_left` `Set.mapsTo_preimage` `Set.inter_subset_right`
`const` 📖	mathematical	—	`LocallyLipschitz`	—	`LipschitzWith.locallyLipschitz` `LipschitzWith.const`
`continuous` 📖	mathematical	`LocallyLipschitz`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`continuous_iff_continuousAt` `ContinuousOn.continuousAt` `LipschitzOnWith.continuousOn`
`id` 📖	mathematical	—	`LocallyLipschitz`	—	`LipschitzWith.locallyLipschitz` `LipschitzWith.id`
`iterate` 📖	mathematical	`LocallyLipschitz`	`Nat.iterate`	—	`id` `Function.iterate_add` `Function.iterate_one` `comp`
`locallyLipschitzOn` 📖	mathematical	`LocallyLipschitz`	`LocallyLipschitzOn`	—	`LocallyLipschitzOn.mono` `locallyLipschitzOn_univ` `Set.subset_univ`
`mul_end` 📖	mathematical	`LocallyLipschitz`	`Function.End` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoidEnd`	—	`comp`
`pow_end` 📖	mathematical	`LocallyLipschitz`	`Function.End` `Monoid.toNatPow` `instMonoidEnd`	—	`pow_zero` `id` `pow_succ` `mul_end`
`prodMk` 📖	mathematical	`LocallyLipschitz`	`Prod.pseudoEMetricSpaceMax`	—	`Filter.inter_mem` `LipschitzOnWith.prodMk` `LipschitzOnWith.mono` `Set.inter_subset_left` `Set.inter_subset_right`
`prodMk_left` 📖	mathematical	—	`LocallyLipschitz` `Prod.pseudoEMetricSpaceMax`	—	`LipschitzWith.locallyLipschitz` `LipschitzWith.prodMk_left`
`prodMk_right` 📖	mathematical	—	`LocallyLipschitz` `Prod.pseudoEMetricSpaceMax`	—	`LipschitzWith.locallyLipschitz` `LipschitzWith.prodMk_right`

LocallyLipschitzOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn` 📖	mathematical	`LocallyLipschitzOn`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`continuousOn_iff_continuous_restrict` `LocallyLipschitz.continuous` `restrict`
`mono` 📖	—	`LocallyLipschitzOn` `Set` `Set.instHasSubset`	—	—	`nhdsWithin_mono`
`restrict` 📖	mathematical	`LocallyLipschitzOn`	`LocallyLipschitz` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	`locallyLipschitzOn_iff_restrict`

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lipschitzOnWith_iff_restrict` 📖	mathematical	`Set.MapsTo`	`LipschitzOnWith` `LipschitzWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `restrict`	—	`lipschitzOnWith_iff_restrict`

(root)

Definitions

Name	Category	Theorems
`LipschitzOnWith` 📖	MathDef	55 math math: `isClosed_setOf_lipschitzOnWith`, `lipschitzOnWith_closure_iff`, `ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith`, `lipschitzOnWith_iff_restrict`, `LipschitzOnWith.of_dist_le_mul`, `lipschitzOnWith_cfc_fun_of_subset`, `IsPicardLindelof.lipschitzOnWith`, `HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt`, `HasStrictFDerivAt.exists_lipschitzOnWith`, `lipschitzOnWith_iff_norm_div_le`, `LipschitzOnWith.mk_one`, `lipschitzOnWith_cfc_fun`, `Convex.lipschitzOnWith_of_nnnorm_fderiv_le`, `lipschitzOnWith_neg_iff`, `Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le`, `Convex.lipschitzOnWith_of_nnnorm_hasDerivWithin_le`, `lipschitzOnWith_cfcₙ_fun`, `Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt`, `HasFTaylorSeriesUpToOn.exists_lipschitzOnWith`, `ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt`, `LipschitzOnWith.coordinate`, `LipschitzOnWith.iff_le_add_mul`, `UniformOnFun.lipschitzOnWith_iff`, `lipschitzOnWith_cfcₙ_fun_of_subset`, `LipschitzOnWith.zero_iff`, `lipschitzOnWith_inv_iff`, `Set.MapsTo.lipschitzOnWith_iff_restrict`, `lipschitzOnWith_iff_dist_le_mul`, `lipschitzOnWith_univ`, `LipschitzOnWith.of_le_add`, `ContDiffOn.exists_lipschitzOnWith`, `ConcaveOn.exists_lipschitzOnWith_of_isBounded`, `ConvexOn.exists_lipschitzOnWith_of_isBounded`, `holderOnWith_one`, `lipschitzOnWith_restrict`, `UniformFun.lipschitzOnWith_ofFun_iff`, `LipschitzWith.lipschitzOnWith`, `LipschitzOnWith.of_le_add_mul'`, `Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt`, `IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith`, `UniformFun.lipschitzOnWith_iff`, `ApproximatesLinearOn.lipschitzOnWith`, `ContDiffAt.exists_lipschitzOnWith`, `ContDiffWithinAt.exists_lipschitzOnWith`, `LipschitzOnWith.of_dist_le'`, `Convex.lipschitzOnWith_of_nnnorm_deriv_le`, `LocallyLipschitzOn.exists_lipschitzOnWith_of_compact`, `LipschitzOnWith.of_le_add_mul`, `lipschitzOnWith_iff_norm_sub_le`, `Convex.lipschitzOnWith_of_nnnorm_fderivWithin_le`, `ConvexOn.lipschitzOnWith_of_abs_le`, `HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt`, `Convex.lipschitzOnWith_of_nnnorm_derivWithin_le`, `lipschitzOnWith_empty`, `ConcaveOn.lipschitzOnWith_of_abs_le`
`LipschitzWith` 📖	MathDef	137 math math: `PiLp.lipschitzWith_toLp`, `LipschitzWith.id`, `LipschitzWith.prodMk_right`, `LinearIsometry.lipschitz`, `LipschitzOnWith.mapsToRestrict`, `ApproximatesLinearOn.lipschitz`, `LipschitzWith.mk_one`, `LipschitzWith.prod_snd`, `AddMonoidHomClass.lipschitz_of_bound_nnnorm`, `IsometryClass.lipschitz`, `EMetric.NonemptyCompacts.lipschitz_prod`, `Complex.lipschitz_equivRealProd`, `TopologicalSpace.Compacts.lipschitz_prod`, `ODE.FunSpace.range_toContinuousMap`, `lipschitzWith_lipschitz_const_add_edist`, `ContDiff.lipschitzWith_of_hasCompactSupport`, `AntilipschitzWith.to_rightInvOn`, `UniformOnFun.lipschitzWith_one_ofFun_toFun`, `AntilipschitzWith.to_rightInverse`, `lipschitzOnWith_iff_restrict`, `lipschitzWith_sup_right`, `LipschitzWith.of_edist_le`, `TopologicalSpace.Compacts.lipschitz_sup`, `SemilinearIsometryClass.lipschitz`, `AddMonoidHomClass.lipschitz_of_bound`, `LipschitzWith.dist_left`, `LipschitzWith.of_le_add`, `AffineIsometry.lipschitz`, `LipschitzWith.prod_fst`, `LipschitzWith.projIcc`, `lipschitzWith_thickenedIndicator`, `ContinuousLinearMap.lipschitz`, `TopologicalSpace.NonemptyCompacts.lipschitz_prod`, `lipschitzWith_one_norm'`, `lipschitzWith_lipschitz_const_mul_edist`, `ContinuousLinearMap.lipschitz_apply`, `LipschitzWith.const'`, `TopologicalSpace.Closeds.lipschitz_sup`, `NNReal.lipschitzWith_sub`, `lipschitzWith_circleMap`, `PiLp.lipschitzWith_ofLp`, `Real.lipschitzWith_sin`, `UniformOnFun.lipschitzWith_iff`, `AffineMap.lipschitzWith_of_finiteDimensional`, `LipschitzMul.lipschitz_mul`, `lipschitzWith_iff_norm_div_le`, `LipschitzOnWith.extend_real`, `MonoidHomClass.lipschitz_of_bound_nnnorm`, `ContinuousLinearMap.lipschitzWith_of_opNorm_le`, `LipschitzWith.coordinate`, `LipschitzOnWith.to_restric_mapsTo`, `LipschitzOnWith.extend_finite_dimension`, `LipschitzOnWith.extend_lp_infty`, `WithLp.prod_lipschitzWith_ofLp`, `MeasureTheory.Lp.lipschitzWith_pos_part`, `PiNat.exists_lipschitz_retraction_of_isClosed`, `lipschitzWith_iff_norm_sub_le`, `ContinuousLinearEquiv.lipschitz`, `UniformFun.lipschitzWith_ofFun_iff`, `ApproximatesLinearOn.lipschitz_sub`, `WithLp.prod_lipschitzWith_toLp`, `UniformOnFun.lipschitzWith_eval`, `RCLike.lipschitzWith_re`, `AntilipschitzWith.to_rightInvOn'`, `lipschitzWith_inv_iff`, `Real.lipschitzWith_one_mulExpNegMulSq`, `ContractingWith.toLipschitzWith`, `MeasureTheory.MeasuredSets.lipschitzWith_measureReal`, `LipschitzWith.dist_right`, `Isometry.lipschitzWith_iff`, `LipschitzWith.prodMk_left`, `LipschitzOnWith.extend_pi`, `lipschitzWith_iff_dist_le_mul`, `lipschitzWith_negPart`, `Real.lipschitzWith_toNNReal`, `LipschitzWith.of_le_add_mul`, `lipschitzWith_of_nnnorm_fderiv_le`, `lipschitzWith_one_nnnorm`, `MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz`, `UniformFun.lipschitzWith_iff`, `LipschitzWith.eval`, `LipschitzWith.iff_le_add_mul`, `Isometry.lipschitz`, `Convex.lipschitz_gauge`, `SeminormedAddCommGroup.lipschitzWith_sub`, `Submodule.lipschitzWith_starProjection`, `BoundedContinuousFunction.lipschitz_compContinuous`, `Set.MapsTo.lipschitzOnWith_iff_restrict`, `lipschitzOnWith_univ`, `TopologicalSpace.NonemptyCompacts.lipschitz_sup`, `GromovHausdorff.toGHSpace_lipschitz`, `Convex.lipschitzWith_gauge`, `NormedAddGroupHom.lipschitz`, `ContinuousLinearMap.opNorm_le_iff_lipschitz`, `RCLike.lipschitzWith_ofReal`, `Metric.lipschitz_infDist_pt`, `Submodule.lipschitzWith_orthogonalProjection`, `LipschitzOnWith.to_restrict`, `lipschitzWith_of_nnnorm_deriv_le`, `Real.lipschitzWith_cos`, `Metric.lipschitz_infDist`, `Dilation.lipschitz`, `EMetric.Closeds.lipschitz_sup`, `AffineIsometryEquiv.lipschitz`, `MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz`, `LinearIsometryEquiv.lipschitz`, `Metric.lipschitz_infDist_set`, `BoundedContinuousFunction.lipschitz_eval_const`, `BoundedContinuousFunction.lipschitz_evalx`, `LipschitzWith.const`, `lipschitzWith_one_nnnorm'`, `MonoidHomClass.lipschitz_of_bound`, `lipschitzWith_max`, `lipschitzWith_lineMap`, `Unitization.lipschitzWith_addEquiv`, `LipschitzWith.of_dist_le_mul`, `lipschitzWith_posPart`, `lipschitzWith_smul`, `EMetric.NonemptyCompacts.lipschitz_sup`, `isClosed_setOf_lipschitzWith`, `lipschitzWith_min`, `LipschitzAdd.lipschitz_add`, `LipschitzWith.of_dist_le'`, `UniformOnFun.lipschitzWith_restrict`, `LipschitzWith.subtype_val`, `Metric.lipschitz_infNndist_pt`, `MeasureTheory.L1.setToL1_lipschitz`, `LipschitzWith.zero_iff`, `ODE.FunSpace.lipschitzWith`, `LipschitzWith.of_le_add_mul'`, `RCLike.lipschitzWith_im`, `lipschitzWith_neg_iff`, `holderWith_one`, `UniformOnFun.lipschitzWith_one_ofFun_toFun'`, `LipschitzWith.dist`, `lipschitzWith_one_norm`, `UniformFun.lipschitzWith_eval`
`LocallyLipschitz` 📖	MathDef	13 math math: `locallyLipschitz_neg_iff`, `ConcaveOn.locallyLipschitz`, `LipschitzWith.locallyLipschitz`, `locallyLipschitzOn_univ`, `LocallyLipschitz.id`, `ConvexOn.locallyLipschitz`, `LocallyLipschitzOn.restrict`, `LocallyLipschitz.prodMk_left`, `ContDiff.locallyLipschitz`, `locallyLipschitz_inv_iff`, `LocallyLipschitz.const`, `locallyLipschitzOn_iff_restrict`, `LocallyLipschitz.prodMk_right`
`LocallyLipschitzOn` 📖	MathDef	15 math math: `ConvexOn.continuousOn_tfae`, `locallyLipschitzOn_univ`, `ConcaveOn.locallyLipschitzOn_interior`, `locallyLipschitzOn_empty`, `locallyLipschitzOn_neg_iff`, `ConvexOn.locallyLipschitzOn_iff_continuousOn`, `LocallyLipschitz.locallyLipschitzOn`, `ConvexOn.locallyLipschitzOn_interior`, `ConvexOn.locallyLipschitzOn`, `ConcaveOn.locallyLipschitzOn`, `ConcaveOn.continuousOn_tfae`, `ContDiffOn.locallyLipschitzOn`, `locallyLipschitzOn_inv_iff`, `ConcaveOn.locallyLipschitzOn_iff_continuousOn`, `locallyLipschitzOn_iff_restrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_prod_of_continuousOn_lipschitzOnWith` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `LipschitzOnWith`	`instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith` `Set.Subset.rfl` `subset_closure`
`continuousOn_prod_of_continuousOn_lipschitzOnWith'` 📖	mathematical	`LipschitzOnWith` `ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`continuousOn_prod_of_continuousOn_lipschitzOnWith` `ContinuousOn.comp` `Continuous.continuousOn` `continuous_swap` `Set.mapsTo_swap_prod`
`continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith` 📖	mathematical	`Set` `Set.instHasSubset` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ContinuousOn` `LipschitzOnWith`	`instTopologicalSpaceProd` `SProd.sprod` `Set.instSProd`	—	`Filter.HasBasis.tendsto_right_iff` `Metric.nhds_basis_closedEBall` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.half_pos` `LT.lt.ne'` `ENNReal.exists_nnreal_pos_mul_lt` `ENNReal.coe_ne_top` `EMetric.mem_closure_iff` `ENNReal.coe_pos` `inter_mem_nhdsWithin` `Metric.eball_mem_nhds` `Filter.inter_mem` `self_mem_nhdsWithin` `Metric.closedEBall_mem_nhds` `Filter.mp_mem` `nhdsWithin_prod` `Filter.univ_mem'` `edist_triangle4` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LipschitzOnWith.edist_le_mul_of_le` `LE.le.trans` `PseudoEMetricSpace.edist_triangle` `le_of_lt` `LT.lt.le` `Eq.trans_le` `PseudoEMetricSpace.edist_comm` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `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` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.mul_one` `add_le_add_left` `ENNReal.add_halves`
`continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith'` 📖	mathematical	`Set` `Set.instHasSubset` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `LipschitzOnWith` `ContinuousOn`	`instTopologicalSpaceProd` `SProd.sprod` `Set.instSProd`	—	`continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith` `ContinuousOn.comp` `Continuous.continuousOn` `continuous_swap` `Set.mapsTo_swap_prod`
`continuous_prod_of_continuous_lipschitzWith` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `LipschitzWith`	`instTopologicalSpaceProd`	—	`continuous_prod_of_dense_continuous_lipschitzWith` `dense_univ`
`continuous_prod_of_continuous_lipschitzWith'` 📖	mathematical	`LipschitzWith` `Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`instTopologicalSpaceProd`	—	`continuous_prod_of_continuous_lipschitzWith` `Continuous.comp` `continuous_swap`
`continuous_prod_of_dense_continuous_lipschitzWith` 📖	mathematical	`Dense` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Continuous` `LipschitzWith`	`instTopologicalSpaceProd`	—	`continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith` `Set.subset_univ` `Eq.ge` `Dense.closure_eq`
`continuous_prod_of_dense_continuous_lipschitzWith'` 📖	mathematical	`Dense` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `LipschitzWith` `Continuous`	`instTopologicalSpaceProd`	—	`continuous_prod_of_dense_continuous_lipschitzWith` `Continuous.comp` `continuous_swap`
`lipschitzOnWith_empty` 📖	mathematical	—	`LipschitzOnWith` `Set` `Set.instEmptyCollection`	—	—
`lipschitzOnWith_iff_restrict` 📖	mathematical	—	`LipschitzOnWith` `LipschitzWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	—
`lipschitzOnWith_restrict` 📖	mathematical	—	`LipschitzOnWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `Set.instInter` `Set.image`	—	`Set.image_val_inter_self_right_eq_coe`
`lipschitzOnWith_univ` 📖	mathematical	—	`LipschitzOnWith` `Set.univ` `LipschitzWith`	—	—
`locallyLipschitzOn_empty` 📖	mathematical	—	`LocallyLipschitzOn` `Set` `Set.instEmptyCollection`	—	—
`locallyLipschitzOn_iff_restrict` 📖	mathematical	—	`LocallyLipschitzOn` `LocallyLipschitz` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	`nhds_subtype_eq_comap_nhdsWithin` `Set.Subset.rfl` `LipschitzOnWith.mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_right` `Set.image_preimage_subset` `Filter.inter_mem` `self_mem_nhdsWithin`
`locallyLipschitzOn_univ` 📖	mathematical	—	`LocallyLipschitzOn` `Set.univ` `LocallyLipschitz`	—	`nhdsWithin_univ`

---

← Back to Index