Theorems · Theorem · general topology
ContractingWith.isFixedPt_fixedPoint_iterate
∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α} [inst_1 : Nonempty α] [inst_2 : CompleteSpace α]
{n : ℕ} (hf : ContractingWith K f^[n]), Function.IsFixedPt f (ContractingWith.fixedPoint f^[n] hf)If a map f has a contracting iterate f^[n], then the fixed point of f^[n] is also a fixed
point of f.
- Defined in
- Mathlib.Topology.MetricSpace.Contracting
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NNRealstatement and proof · cited by 4,310
- one_mulproof · cited by 2,841
- CompleteSpacestatement and proof · cited by 2,532
- MetricSpacestatement and proof · cited by 1,684
- Dist.distproof · cited by 1,539
- NNReal.toRealproof · cited by 1,260
- Nat.iteratestatement and proof · cited by 740
- Function.IsFixedPtstatement and proof · cited by 84
- Function.iterate_succ_apply'proof · cited by 72
- mul_lt_mul_of_pos_rightproof · cited by 54
- ContractingWithstatement and proof · cited by 39
- LipschitzWith.dist_le_mulproof · cited by 20
Cited by1
Results whose statement or proof uses this declaration.
- ODE.FunSpace.exists_isFixedPt_nextproof · cited by 3