Theorems · Theorem · general topology
ContractingWith.eq_or_edist_eq_top_of_fixedPoints
∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α},
ContractingWith K f → ∀ {x y : α}, Function.IsFixedPt f x → Function.IsFixedPt f y → x = y ∨ edist x y = ⊤- Defined in
- Mathlib.Topology.MetricSpace.Contracting
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 153 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.
Cites13
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
- ENNReal.ofNNRealproof · 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
- ENNReal.zero_divproof · cited by 24
- Function.IsFixedPt.eqproof · cited by 14
- edist_le_zeroproof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- ContractingWith.fixedPoint_unique'proof · cited by 1
- ContractingWith.efixedPoint_eq_of_edist_lt_topproof · cited by 0
- ContractingWith.efixedPoint_eq_of_edist_lt_top'proof · cited by 0