English
Post-composition by an isometry does not change the Lipschitz-property of a function.
Русский
Пост-обратное композиционное по изометрии не изменяет липшицевость функции.
LaTeX
$$$\forall \alpha\,\beta\,\gamma\,[\text{PseudoMetricSpace }\alpha][\text{PseudoMetricSpace }\beta][\text{PseudoMetricSpace }\gamma] \\ {f:\alpha\to\beta}\,{g:\beta\to\gamma}\, (K:\mathbb{R}_{\ge 0})\,:\nLipschitzWith K (g \circ f) \iff LipschitzWith K f$$
Lean4
/-- Post-composition by an isometry does not change the Lipschitz-property of a function. -/
theorem lipschitzWith_iff {α β γ : Type*} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ]
{f : α → β} {g : β → γ} (K : ℝ≥0) (h : Isometry g) : LipschitzWith K (g ∘ f) ↔ LipschitzWith K f := by
simp [LipschitzWith, h.edist_eq]
