Theorems · Theorem · general topology

isBounded_iff_of_bilipschitz

∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K₁ K₂ : NNReal}
  {f : α → β},
  AntilipschitzWith K₁ f → LipschitzWith K₂ f → ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s

If f : α → β is bilipschitz, then the pullback of the bornology on β through f agrees with the bornology on α. This can be used to provide the replacement equality when applying PseudoMetricSpace.replaceBornology, which can be useful when following the forgetful inheritance pattern when creating type synonyms. Important Note: if α is some synonym of a type β (at default transparency), and f : α ≃ β is some bilipschitz equivalence, then instead of writing: `` instance : Bornology α := inferInstanceAs (Bornology β) ` Users should instead write something like: ` instance : Bornology α := Bornology.induced (f : α → β) ` in order to avoid abuse of the definitional equality α := β`.

Defined in

Mathlib.Topology.MetricSpace.Bilipschitz

Cited by

0 results in Mathlib

Foundations

Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpacePseudoMetricSpace