English
Composition in the target of a bounded continuous function with a Lipschitz map yields a bounded continuous function.
Русский
Композиция ограниченной непрерывной функции в целевом пространстве с липшицевой картой даёт ограниченную непрерывную функцию.
LaTeX
$$def comp (G : β → γ) {C : NNReal} (H : LipschitzWith C G) (f : α →ᵇ β) : α →ᵇ γ$$
Lean4
/-- Composition (in the target) of a bounded continuous function with a Lipschitz map again
gives a bounded continuous function. -/
def comp (G : β → γ) {C : ℝ≥0} (H : LipschitzWith C G) (f : α →ᵇ β) : α →ᵇ γ :=
⟨⟨fun x => G (f x), H.continuous.comp f.continuous⟩,
let ⟨D, hD⟩ := f.bounded
⟨max C 0 * D, fun x y =>
calc
dist (G (f x)) (G (f y)) ≤ C * dist (f x) (f y) := H.dist_le_mul _ _
_ ≤ max C 0 * dist (f x) (f y) := by gcongr; apply le_max_left
_ ≤ max C 0 * D := by gcongr; apply hD⟩⟩
