[Merged by Bors] - feat: locally Lipschitz maps

[grunweg]

Define locally Lipschitz maps and show their basic properties.
In particular, they are continuous and stable under composition and products.
As an application, we conclude that C¹ maps are locally Lipschitz.

---

I've gone through the entire file; all API for Lipschitz maps (where this makes sense) has a counterpart for locally Lipschitz maps.

Left for the future:

• sum and scalar multiples of a locally Lipschitz function valued in a normed space is locally Lipschitz
  (hence, locally Lipschitz functions form a submodule of the ring of continuous functions)
• locally Lipschitz maps are a submonoid of $\text{End}(\alpha)$
• both of these also hold for Lipschitz maps (on a set)

[grunweg]

For the proof of composition, I'm stuck on two sorries related to coercions of subsets. Minimized code:

import Mathlib.Topology.EMetricSpace.Basic
open Topology
lemma minimized {X Y Z: Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : Y → Z} {g : X → Y} {t: Set X} {u: Set Y}
    {x : X} (ht: t ∈ 𝓝 x) (hu: u ∈ 𝓝 (g x)) : True /- dummy statement -/ := by
  -- idea: shrink u to g(t); more precisely:
  -- restrict g to t' := t ∩ g⁻¹(u); the preimage of u under g':=g∣t.
  let g' := t.restrict g
  let t' : Set X := ↑(g' ⁻¹' u)
  -- The following is mathematically easy; I'm wrestling with filling the sorries.
  have h₁ : t' = t ∩ g ⁻¹' u := by
    apply Iff.mpr (Set.Subset.antisymm_iff)
    constructor
    · intro x hx
      constructor
      · exact Set.coe_subset hx
      · -- goal: x ∈ g ⁻¹' u
        -- informal argument: as x ∈ t', we can apply g' (and land in u by definition), so g'(x)=g(x) ∈ u
        sorry
    · intro x hx
      rcases hx with ⟨ht, hgu⟩
      -- goal: x ∈ t'
      -- as x ∈ t, we can write g(x)=g'(x); the rhs lies in u, so x ∈ g⁻¹(u) also
      sorry
  sorry -- omitted (have proven this)

[grunweg]

@eric-wieser Thanks for the quick comments. I've made the requested changes.
I'm on the fence about the second: it enables more golfing; in general, I find these golfed proofs somewhat readable in VS Code, but not on github. I don't know if the latter is aimed for; your call as a maintainer.

[grunweg]

Fixed the last sorry - courtesy of Alex J. Best on zulip. Thanks!
(There's also an aesop-free version, if you'd prefer me to avoid such a heavy hammer.)

[grunweg]

awaiting-review

[sgouezel]

bors d+
Thanks!

[bors]

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grunweg]

Thanks for the review!
bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style