# Bilipschitz equivalence #

A common pattern in Mathlib is to replace the topology, uniformity and bornology on a type synonym with those of the underlying type.

The most common way to do this is to activate a local instance for something which puts a
`PseudoMetricSpace`

structure on the type synonym, prove that this metric is bilipschitz equivalent
to the metric on the underlying type, and then use this to show that the uniformities and
bornologies agree, which can then be used with `PseudoMetricSpace.replaceUniformity`

or
`PseudoMetricSpace.replaceBornology`

.

With the tooling outside this file, this can be a bit cumbersome, especially when it occurs repeatedly, and moreover it can lend itself to abuse of the definitional equality inherent in the type synonym. In this file, we make this pattern more convenient by providing lemmas which take directly the conditions that the map is bilipschitz, and then prove the relevant equalities. Moreover, because there are no type synonyms here, it is necessary to phrase these equalities in terms of the induced uniformity and bornology, which means users will need to do the same if they choose to use these convenience lemmas. This encourages good hygiene in the development of type synonyms.

If `f : α → β`

is bilipschitz, then the pullback of the uniformity on `β`

through `f`

agrees
with the uniformity on `α`

.

This can be used to provide the replacement equality when applying
`PseudoMetricSpace.replaceUniformity`

, 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 : UniformSpace α := inferInstanceAs (UniformSpace β)
```

Users should instead write something like:

```
instance : UniformSpace α := (inferInstance : UniformSpace β).comap f
```

in order to avoid abuse of the definitional equality `α := β`

.

If `f : α → β`

is bilipschitz, then the pullback of the bornology on `β`

through `f`

agrees
with the bornology on `α`

.

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 `α := β`

.