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_restrict, uniformContinuousOn, weaken, 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	LipschitzOnWith NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	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	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 📖	mathematical	LipschitzOnWith Set Set.instMembership ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.ofNNReal	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	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 📖	mathematical	LipschitzOnWith Set Set.instHasSubset	LipschitzOnWith	—	—
prodMk 📖	mathematical	LipschitzOnWith	LipschitzOnWith Prod.pseudoEMetricSpaceMax NNReal SemilatticeSup.toMax NNReal.instSemilatticeSup	—	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_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
weaken 📖	mathematical	LipschitzOnWith NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder	LipschitzOnWith	—	LE.le.trans mul_left_mono covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid ENNReal.coe_le_coe
zero_iff 📖	mathematical	—	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace NNReal NNReal.instZero	—	MulZeroClass.zero_mul ENNReal.instCanonicallyOrderedAdd

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	LipschitzWith	LipschitzWith NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	mul_right_mono IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid mul_assoc ENNReal.coe_mul
comp_lipschitzOnWith 📖	mathematical	LipschitzWith LipschitzOnWith	LipschitzOnWith NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	lipschitzOnWith_iff_restrict comp LipschitzOnWith.to_restrict
const 📖	mathematical	—	LipschitzWith NNReal NNReal.instZero	—	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.toPow 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	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	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
edist_lt_of_edist_lt_div 📖	mathematical	LipschitzWith ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.ofNNReal	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist	—	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 NNReal.instOne Function.eval	—	of_edist_le edist_le_pi_edist
id 📖	mathematical	—	LipschitzWith NNReal NNReal.instOne	—	of_edist_le le_rfl
iterate 📖	mathematical	LipschitzWith	LipschitzWith NNReal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instSemiring Nat.iterate	—	pow_zero id pow_succ comp
lipschitzOnWith 📖	mathematical	LipschitzWith	LipschitzOnWith	—	—
list_prod 📖	mathematical	LipschitzWith	LipschitzWith NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring NNReal.instOne 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	LipschitzWith NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring 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 NNReal.instOne	—	one_mul
pow_end 📖	mathematical	LipschitzWith	LipschitzWith NNReal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instSemiring Function.End instMonoidEnd	—	pow_zero id pow_succ mul_end
prodMk 📖	mathematical	LipschitzWith	LipschitzWith Prod.pseudoEMetricSpaceMax NNReal SemilatticeSup.toMax NNReal.instSemilatticeSup	—	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 NNReal.instOne	—	max_eq_right zero_le_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass prodMk const id
prodMk_right 📖	mathematical	—	LipschitzWith Prod.pseudoEMetricSpaceMax NNReal NNReal.instOne	—	max_eq_left zero_le_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass prodMk id const
prod_fst 📖	mathematical	—	LipschitzWith Prod.pseudoEMetricSpaceMax NNReal NNReal.instOne	—	of_edist_le le_max_left
prod_snd 📖	mathematical	—	LipschitzWith Prod.pseudoEMetricSpaceMax NNReal NNReal.instOne	—	of_edist_le le_max_right
restrict 📖	mathematical	LipschitzWith	LipschitzWith Set.Elem instPseudoEMetricSpaceSubtype Set Set.instMembership Set.restrict	—	—
subtype_mk 📖	mathematical	LipschitzWith	LipschitzWith instPseudoEMetricSpaceSubtype	—	—
subtype_val 📖	mathematical	—	LipschitzWith Set Set.instMembership instPseudoEMetricSpaceSubtype NNReal NNReal.instOne	—	of_edist_le le_rfl
uncurry 📖	mathematical	LipschitzWith	LipschitzWith Prod.pseudoEMetricSpaceMax NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	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 📖	mathematical	LipschitzWith NNReal Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder	LipschitzWith	—	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 NNReal.instZero	—	MulZeroClass.zero_mul ENNReal.instCanonicallyOrderedAdd

LocallyLipschitz

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	LocallyLipschitz	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	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	LocallyLipschitz Function.End MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoidEnd	—	comp
pow_end 📖	mathematical	LocallyLipschitz	LocallyLipschitz Function.End Monoid.toPow instMonoidEnd	—	pow_zero id pow_succ mul_end
prodMk 📖	mathematical	LocallyLipschitz	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 📖	mathematical	LocallyLipschitzOn Set Set.instHasSubset	LocallyLipschitzOn	—	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	71 math math: LipschitzOnWith.mono, isClosed_setOf_lipschitzOnWith, LipschitzOnWith.neg, LipschitzOnWith.of_inv, lipschitzOnWith_closure_iff, LipschitzOnWith.sub, LipschitzOnWith.closure, ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith, lipschitzOnWith_iff_restrict, lipschitzOnWith_iff_norm_inv_mul_le, LipschitzOnWith.of_dist_le_mul, lipschitzOnWith_cfc_fun_of_subset, LipschitzOnWith.prodMk, IsPicardLindelof.lipschitzOnWith, HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt, HasStrictFDerivAt.exists_lipschitzOnWith, LipschitzWith.comp_lipschitzOnWith, lipschitzOnWith_iff_norm_div_le, LipschitzOnWith.mk_one, lipschitzOnWith_cfc_fun, Convex.lipschitzOnWith_of_nnnorm_fderiv_le, LipschitzOnWith.of_neg, 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, LipschitzOnWith.add, 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, lipschitzOnWith_iff_norm_neg_add_le, 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, LipschitzOnWith.comp, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith, UniformFun.lipschitzOnWith_iff, LipschitzOnWith.div, 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.weaken, LipschitzOnWith.mul, LipschitzOnWith.inv, 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	171 math math: PiLp.lipschitzWith_toLp, LipschitzWith.max_const, LipschitzWith.id, LipschitzWith.prodMk_right, LinearIsometry.lipschitz, LipschitzOnWith.mapsToRestrict, ApproximatesLinearOn.lipschitz, LipschitzWith.mk_one, LipschitzWith.prod_snd, AddMonoidHomClass.lipschitz_of_bound_nnnorm, LipschitzWith.lipschitzWith_compLp, IsometryClass.lipschitz, EMetric.NonemptyCompacts.lipschitz_prod, Complex.lipschitz_equivRealProd, TopologicalSpace.Compacts.lipschitz_prod, LipschitzWith.completion_extension, 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, LipschitzWith.mul_end, AddMonoidHomClass.lipschitz_of_bound, LipschitzWith.dist_left, LipschitzWith.of_le_add, AffineIsometry.lipschitz, LipschitzWith.prod_fst, LipschitzWith.pow_end, LipschitzWith.projIcc, Dense.lipschitzWith_extend, lipschitzWith_thickenedIndicator, ContinuousLinearMap.lipschitz, TopologicalSpace.NonemptyCompacts.lipschitz_prod, LipschitzWith.list_prod, lipschitzWith_one_norm', lipschitzWith_lipschitz_const_mul_edist, BoundedContinuousFunction.lipschitz_comp, ContinuousLinearMap.lipschitz_apply, LipschitzWith.const', LipschitzWith.inv, TopologicalSpace.Closeds.lipschitz_sup, NNReal.lipschitzWith_sub, lipschitzWith_circleMap, LipschitzWith.min, PiLp.lipschitzWith_ofLp, Real.lipschitzWith_sin, LipschitzWith.prodMk, UniformOnFun.lipschitzWith_iff, AffineMap.lipschitzWith_of_finiteDimensional, LipschitzMul.lipschitz_mul, LipschitzWith.min_const, lipschitzWith_iff_norm_div_le, LipschitzOnWith.extend_real, MonoidHomClass.lipschitz_of_bound_nnnorm, ContinuousLinearMap.lipschitzWith_of_opNorm_le, LipschitzWith.coordinate, 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, LipschitzWith.vadd, ContinuousLinearEquiv.lipschitz, UniformFun.lipschitzWith_ofFun_iff, LipschitzWith.const_min, ApproximatesLinearOn.lipschitz_sub, lp.lipschitzWith_one_eval, LipschitzWith.uncurry, WithLp.prod_lipschitzWith_toLp, LipschitzWith.add, UniformOnFun.lipschitzWith_eval, RCLike.lipschitzWith_re, AntilipschitzWith.to_rightInvOn', lipschitzWith_inv_iff, TopologicalSpace.Closeds.lipschitz_prod, Real.lipschitzWith_one_mulExpNegMulSq, ContractingWith.toLipschitzWith, LipschitzWith.of_neg, LipschitzWith.sub, LipschitzWith.subtype_mk, LipschitzWith.vsub, MeasureTheory.MeasuredSets.lipschitzWith_measureReal, LipschitzWith.iterate, LipschitzWith.dist_right, Isometry.lipschitzWith_iff, LipschitzWith.restrict, LipschitzWith.neg, LipschitzWith.completion_map, 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.max, lipschitzWith_one_nnnorm, MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz, UniformFun.lipschitzWith_iff, LipschitzWith.eval, LipschitzWith.iff_le_add_mul, Isometry.lipschitz, Convex.lipschitz_gauge, LipschitzWith.mul, SeminormedAddCommGroup.lipschitzWith_sub, Submodule.lipschitzWith_starProjection, BoundedContinuousFunction.lipschitz_compContinuous, Set.MapsTo.lipschitzOnWith_iff_restrict, lipschitzOnWith_univ, TopologicalSpace.NonemptyCompacts.lipschitz_sup, LipschitzWith.weaken, GromovHausdorff.toGHSpace_lipschitz, LipschitzWith.comp, 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', lipschitzWith_iff_norm_inv_mul_le, MonoidHomClass.lipschitz_of_bound, lipschitzWith_max, lipschitzWith_lineMap, Unitization.lipschitzWith_addEquiv, lipschitzWith_iff_norm_neg_add_le, LipschitzWith.of_dist_le_mul, lipschitzWith_posPart, lipschitzWith_smul, LipschitzWith.const_max, 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, LipschitzWith.of_inv, LipschitzWith.div, 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	32 math math: locallyLipschitz_neg_iff, LocallyLipschitz.prodMk, ConcaveOn.locallyLipschitz, LipschitzWith.locallyLipschitz, locallyLipschitzOn_univ, LocallyLipschitz.mul, LocallyLipschitz.id, LocallyLipschitz.comp, LocallyLipschitz.div, LocallyLipschitz.inv, LocallyLipschitz.iterate, ConvexOn.locallyLipschitz, LocallyLipschitz.const_max, LocallyLipschitz.max, LocallyLipschitzOn.restrict, LocallyLipschitz.of_inv, LocallyLipschitz.pow_end, LocallyLipschitz.min_const, LocallyLipschitz.of_neg, LocallyLipschitz.prodMk_left, ContDiff.locallyLipschitz, LocallyLipschitz.sub, LocallyLipschitz.max_const, LocallyLipschitz.neg, LocallyLipschitz.mul_end, LocallyLipschitz.const_min, locallyLipschitz_inv_iff, LocallyLipschitz.add, LocallyLipschitz.const, LocallyLipschitz.min, locallyLipschitzOn_iff_restrict, LocallyLipschitz.prodMk_right
LocallyLipschitzOn 📖	MathDef	24 math math: ConvexOn.continuousOn_tfae, locallyLipschitzOn_univ, LocallyLipschitzOn.neg, ConcaveOn.locallyLipschitzOn_interior, LocallyLipschitzOn.add, locallyLipschitzOn_empty, locallyLipschitzOn_neg_iff, LocallyLipschitzOn.mono, LocallyLipschitzOn.sub, LocallyLipschitzOn.of_neg, ConvexOn.locallyLipschitzOn_iff_continuousOn, LocallyLipschitz.locallyLipschitzOn, ConvexOn.locallyLipschitzOn_interior, LocallyLipschitzOn.div, ConvexOn.locallyLipschitzOn, ConcaveOn.locallyLipschitzOn, ConcaveOn.continuousOn_tfae, LocallyLipschitzOn.inv, ContDiffOn.locallyLipschitzOn, locallyLipschitzOn_inv_iff, LocallyLipschitzOn.mul, ConcaveOn.locallyLipschitzOn_iff_continuousOn, LocallyLipschitzOn.of_inv, locallyLipschitzOn_iff_restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_prod_of_continuousOn_lipschitzOnWith 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace LipschitzOnWith	ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace 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	ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace 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	ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace SProd.sprod Set 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	ContinuousOn instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace SProd.sprod Set 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	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	continuous_prod_of_dense_continuous_lipschitzWith dense_univ
continuous_prod_of_continuous_lipschitzWith' 📖	mathematical	LipschitzWith Continuous UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	continuous_prod_of_continuous_lipschitzWith Continuous.comp continuous_swap
continuous_prod_of_dense_continuous_lipschitzWith 📖	mathematical	Dense UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace Continuous LipschitzWith	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	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	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	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