Theorems · Theorem · general topology

ContractingWith.apriori_edist_iterate_efixedPoint_le

∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [inst_1 : CompleteSpace α] (hf : ContractingWith K f)
  {x : α} (hx : edist x (f x) ≠ ⊤) (n : ℕ),
  edist (f^[n] x) (ContractingWith.efixedPoint f hf x hx) ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)

Defined in

Mathlib.Topology.MetricSpace.Contracting

Cited by

1 results in Mathlib

Foundations

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

Assumes

EMetricSpaceCompleteSpace