English
A function f is 1-Lipschitz iff for all x,y,n, y ∈ cylinder(x,n) implies dist(fx,fy) ≤ (1/2)^n.
Русский
Функция f является 1-Lipschitz тогда и только тогда, когда для любых x,y,n, если y ∈ цилиндр(x,n), то dist(fx,fy) ≤ (1/2)^n.
LaTeX
$$$$ \bigl(\forall x,y,\operatorname{dist}(f(x),f(y)) \le \operatorname{dist}(x,y)\bigr) \iff \forall x,y,n,\; y\in \mathrm{cylinder}(x,n) \Rightarrow \operatorname{dist}(f(x),f(y)) \le (1/2)^n $$$$
Lean4
/-- A function to a pseudo-metric-space is `1`-Lipschitz if and only if points in the same cylinder
of length `n` are sent to points within distance `(1/2)^n`.
Not expressed using `LipschitzWith` as we don't have a metric space structure -/
theorem lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder {α : Type*} [PseudoMetricSpace α]
{f : (∀ n, E n) → α} :
(∀ x y : ∀ n, E n, dist (f x) (f y) ≤ dist x y) ↔ ∀ x y n, y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n :=
by
constructor
· intro H x y n hxy
apply (H x y).trans
rw [PiNat.dist_comm]
exact mem_cylinder_iff_dist_le.1 hxy
· intro H x y
rcases eq_or_ne x y with (rfl | hne)
· simp [PiNat.dist_nonneg]
rw [dist_eq_of_ne hne]
apply H x y (firstDiff x y)
rw [firstDiff_comm]
exact mem_cylinder_firstDiff _ _
