Theorems · Theorem · general topology

PiNat.lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder

∀ {E : ℕ → Type u_1} {α : Type u_2} [inst : PseudoMetricSpace α] {f : ((n : ℕ) → E n) → α},
  (∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) ↔
    ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ PiNat.cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n

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

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

0 results in Mathlib

Foundations

Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpace