English
If h(x) bounds |f(x)−f(y)| by d(x,y) on s, then f is 1-Lipschitz on s.
Русский
Если граничение на разность значений функции на s по расстоянию верно, то f — 1- Lipschitz на s.
LaTeX
$$$\\forall x\\in s,\\forall y\\in s:\\; d(f(x),f(y)) \\le d(x,y) \\Rightarrow \\operatorname{LipschitzOnWith}(1,f,s)$$$
Lean4
/-- The preimage of a proper space under a Lipschitz proper map is proper. -/
theorem properSpace {X Y : Type*} [PseudoMetricSpace X] [PseudoMetricSpace Y] [ProperSpace Y] {f : X → Y}
(hf : IsProperMap f) {K : ℝ≥0} (hf' : LipschitzWith K f) : ProperSpace X :=
⟨fun x r ↦
(hf.isCompact_preimage (isCompact_closedBall (f x) (K * r))).of_isClosed_subset Metric.isClosed_closedBall
(hf'.mapsTo_closedBall x r).subset_preimage⟩
