Theorems · Theorem · general topology
LipschitzWith.dist_le_mul
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x yAlias of the forward direction of lipschitzWith_iff_dist_le_mul.
- Defined in
- Mathlib.Topology.MetricSpace.Lipschitz
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.diststatement · cited by 1,539
- NNReal.toRealstatement · cited by 1,260
- LipschitzWithstatement · cited by 316
- lipschitzWith_iff_dist_le_mulproof · cited by 10
Cited by20
Results whose statement or proof uses this declaration.
- LipschitzWith.dist_le_mul_of_leproof · cited by 3
- ODE.FunSpace.mem_closedBallproof · cited by 3
- LipschitzWith.norm_le_mulproof · cited by 2
- LipschitzWith.dist_iterate_succ_le_geometricproof · cited by 2
- BoundedContinuousFunction.norm_compContinuous_leproof · cited by 2
- AntilipschitzWith.add_lipschitzWithproof · cited by 2
- BoundedContinuousFunction.lipschitz_compproof · cited by 2
- ContractingWith.dist_le_mulproof · cited by 1
- LipschitzWith.completion_extensionproof · cited by 1
- LipschitzWith.norm_compLp_sub_leproof · cited by 1
- LipschitzOnWith.extend_piproof · cited by 1
- LipschitzWith.norm_le_mul'proof · cited by 1