Bilipschitz

Statistics

Metric	Count
Definitions	0
Theorems `bornology_eq_of_bilipschitz`, `isBounded_iff_of_bilipschitz`, `uniformity_eq_of_bilipschitz`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`bornology_eq_of_bilipschitz` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `LipschitzWith`	`Bornology.cobounded` `Bornology.induced` `PseudoMetricSpace.toBornology`	—	`le_antisymm` `LipschitzWith.comap_cobounded_le` `Filter.Tendsto.le_comap` `AntilipschitzWith.tendsto_cobounded`
`isBounded_iff_of_bilipschitz` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `LipschitzWith`	`Bornology.IsBounded` `Bornology.induced` `PseudoMetricSpace.toBornology`	—	`Filter.ext_iff` `bornology_eq_of_bilipschitz`
`uniformity_eq_of_bilipschitz` 📖	mathematical	`AntilipschitzWith` `LipschitzWith`	`uniformity` `UniformSpace.comap` `UniformSpace` `PseudoEMetricSpace.toUniformSpace`	—	`IsUniformInducing.comap_uniformity` `AntilipschitzWith.isUniformInducing` `LipschitzWith.uniformContinuous`

---