Theorems · Theorem · general topology
LipschitzWith.continuous
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → Continuous fA Lipschitz function is continuous.
- Defined in
- Mathlib.Topology.EMetricSpace.Lipschitz
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Continuousstatement · cited by 2,592
- PseudoEMetricSpacestatement and proof · cited by 1,536
- LipschitzWithstatement and proof · cited by 316
- UniformContinuous.continuousproof · cited by 66
- LipschitzWith.uniformContinuousproof · cited by 33
Cited by30
Results whose statement or proof uses this declaration.
- Isometry.continuousproof · cited by 23
- continuous_posPartproof · cited by 12
- continuous_negPartproof · cited by 9
- LipschitzWith.comp_memLpproof · cited by 6
- ContractingWith.exists_fixedPointproof · cited by 4
- LipschitzWith.coeFn_compLpproof · cited by 3
- LipschitzWith.ae_lineDifferentiableAtproof · cited by 3
- LipschitzWith.memLp_lineDerivproof · cited by 2
- AddMonoidHomClass.continuous_of_boundproof · cited by 2
- MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_subproof · cited by 2
- Convexity.continuous_convexCombPairproof · cited by 2
- Dense.lipschitzWith_extendproof · cited by 1