Theorems · Theorem · general topology

ContractingWith.tendsto_iterate_fixedPoint

∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} (hf : ContractingWith K f) [inst_1 : Nonempty α]
  [inst_2 : CompleteSpace α] (x : α),
  Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds (ContractingWith.fixedPoint f hf))

Defined in: Mathlib.Topology.MetricSpace.Contracting
Cited by: 1 results in Mathlib
Foundations: Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MetricSpace Nonempty CompleteSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpaceproof · cited by 24,529
Filterproof · cited by 8,121
nhdsstatement and proof · cited by 5,554
NNRealstatement and proof · cited by 4,310
Filter.Tendstostatement and proof · cited by 3,814
CompleteSpacestatement and proof · cited by 2,532
Filter.atTopstatement and proof · cited by 2,405
MetricSpacestatement and proof · cited by 1,684
Nat.iteratestatement and proof · cited by 740
ContractingWithstatement and proof · cited by 39
edist_ne_topproof · cited by 17
ContractingWith.fixedPointstatement and proof · cited by 9

Cited by1

Results whose statement or proof uses this declaration.

ODE.FunSpace.exists_forall_closedBall_funSpace_dist_le_mulproof · cited by 1