Theorems · Theorem · general topology
ContractingWith.dist_le_of_fixedPoint
∀ {α : Type u_1} [inst : MetricSpace α] {K : NNReal} {f : α → α},
ContractingWith K f → ∀ (x : α) {y : α}, Function.IsFixedPt f y → dist x y ≤ dist x (f x) / (1 - ↑K)- Defined in
- Mathlib.Topology.MetricSpace.Contracting
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- NNRealstatement and proof · cited by 4,310
- add_zeroproof · cited by 2,707
- MetricSpacestatement and proof · cited by 1,684
- Dist.diststatement and proof · cited by 1,539
- NNReal.toRealstatement and proof · cited by 1,260
- dist_selfproof · cited by 116
- Function.IsFixedPtstatement and proof · cited by 84
- ContractingWithstatement and proof · cited by 39
- Function.IsFixedPt.eqproof · cited by 14
- ContractingWith.dist_inequalityproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le'proof · cited by 1
- ContractingWith.dist_fixedPoint_leproof · cited by 1