Theorems · Theorem · general topology
ContractingWith.edist_le_of_fixedPoint
∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
ContractingWith K f → ∀ {x y : α}, edist x y ≠ ⊤ → Function.IsFixedPt f y → edist x y ≤ edist x (f x) / (1 - ↑K)- Defined in
- Mathlib.Topology.MetricSpace.Contracting
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- EMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- NNRealstatement and proof · cited by 4,310
- add_zeroproof · cited by 2,707
- ENNReal.ofNNRealstatement and proof · cited by 1,279
- EDist.ediststatement and proof · cited by 735
- EMetricSpacestatement and proof · cited by 242
- Function.IsFixedPtstatement and proof · cited by 84
- PseudoEMetricSpace.edist_selfproof · cited by 50
- ContractingWithstatement and proof · cited by 39
- Function.IsFixedPt.eqproof · cited by 14
- ContractingWith.edist_inequalityproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- ContractingWith.eq_or_edist_eq_top_of_fixedPointsproof · cited by 3