Theorems · Theorem · general topology

ContractingWith.efixedPoint_eq_of_edist_lt_top

∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [inst_1 : CompleteSpace α] (hf : ContractingWith K f)
  {x : α} (hx : edist x (f x) ≠ ⊤) {y : α} (hy : edist y (f y) ≠ ⊤),
  edist x y ≠ ⊤ → ContractingWith.efixedPoint f hf x hx = ContractingWith.efixedPoint f hf y hy

Defined in

Mathlib.Topology.MetricSpace.Contracting

Cited by

0 results in Mathlib

Foundations

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

Assumes

EMetricSpaceCompleteSpace