Theorems · Theorem · general topology

ContractingWith.edist_inequality

∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
  ContractingWith K f → ∀ {x y : α}, edist x y ≠ ⊤ → edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - ↑K)

Defined in

Mathlib.Topology.MetricSpace.Contracting

Cited by

1 results in Mathlib

Foundations

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

Assumes

EMetricSpace