Lipschitz maps from extended metric spaces

This file gives a real-valued Lipschitz estimate for the extended distance from a fixed point, shows that the inclusion of a subset into a larger subset is 1-Lipschitz, and shows that composing a function locally Lipschitz on a set with a locally Lipschitz map keeps it locally Lipschitz on that set.

The declaration TauCeti.lipschitzWith_toReal_edist and its proof follow Mathlib pull request #41839, available under Apache 2.0.

theorem TauCeti.lipschitzWith_toReal_edist {X : Type u_1} [PseudoEMetricSpace X] (a : X) : LipschitzWith 1 fun (x : X) => (edist a x).toReal

Distance from a fixed point, converted to a real number, is 1-Lipschitz.

theorem LipschitzWith.inclusion {α : Type u_1} [PseudoEMetricSpace α] {s t : Set α} (h : s ⊆ t) : LipschitzWith 1 (Set.inclusion h)

The inclusion of a subset into a larger subset is 1-Lipschitz.

theorem LocallyLipschitz.comp_locallyLipschitzOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β → γ} {f : α → β} {s : Set α} (hg : LocallyLipschitz g) (hf : LocallyLipschitzOn s f) : LocallyLipschitzOn s (g ∘ f)

A locally Lipschitz map composed with a function locally Lipschitz on s is locally Lipschitz on s.