Theorems · Theorem · general topology

Isometry.lipschitzWith_iff

∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {f : α → β} {g : β → γ} (K : NNReal),
  Isometry g → (LipschitzWith K (g ∘ f) ↔ LipschitzWith K f)

Post-composition by an isometry does not change the Lipschitz-property of a function.

Defined in: Mathlib.Topology.MetricSpace.Isometry
Cited by: 1 results in Mathlib
Foundations: Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoEMetricSpace PseudoEMetricSpace PseudoEMetricSpace

Mathlib docs Source Loogle LeanSearch

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.

NNRealstatement and proof · cited by 4,310
PseudoEMetricSpacestatement and proof · cited by 1,536
ENNReal.ofNNRealproof · cited by 1,279
EDist.edistproof · cited by 735
LipschitzWithstatement · cited by 316
Isometrystatement and proof · cited by 230
Isometry.edist_eqproof · cited by 18

Cited by1

Results whose statement or proof uses this declaration.

NNReal.lipschitzWith_subproof · cited by 0