English
If f: α → ℝ≥0∞ satisfies a linear bound with edist, then f is continuous.
Русский
Если функция удовлетворяет линейному ограничению через edist, то она непрерывна.
LaTeX
$$$\text{Continuous}(f)\;\text{when } f(x) \le f(y) + C \cdot \mathrm{edist}(x,y)$ for some finite C.$$
Lean4
theorem continuous_of_le_add_edist {f : α → ℝ≥0∞} (C : ℝ≥0∞) (hC : C ≠ ∞) (h : ∀ x y, f x ≤ f y + C * edist x y) :
Continuous f :=
by
refine continuous_iff_continuousAt.2 fun x => ENNReal.tendsto_nhds_of_Icc fun ε ε0 => ?_
rcases ENNReal.exists_nnreal_pos_mul_lt hC ε0.ne' with ⟨δ, δ0, hδ⟩
rw [mul_comm] at hδ
filter_upwards [EMetric.closedBall_mem_nhds x (ENNReal.coe_pos.2 δ0)] with y hy
refine ⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩ <;>
refine add_le_add_left (le_trans (mul_le_mul_left' ?_ _) hδ.le) _
exacts [EMetric.mem_closedBall'.1 hy, EMetric.mem_closedBall.1 hy]
