Commit 2024-07-18 00:30 afd433b2

View on Github →

feat: Locally Lipschitz functions on a set (#13990) Define LocallyLipschitzOn, the restricted version of LocallyLipschitz.

Estimated changes

added theorem comap_nhdsWithin_range
deleted theorem comap_nhdsWithin_range
modified theorem nhdsWithin_univ
modified theorem LipschitzOnWith.mono
modified def LipschitzOnWith
modified def LipschitzWith
modified def LocallyLipschitz
modified theorem lipschitzOnWith_empty
added theorem lipschitzOnWith_univ
deleted theorem lipschitzOn_univ