# Dilations #

We define dilations, i.e., maps between emetric spaces that satisfy `edist (f x) (f y) = r * edist x y` for some `r ∉ {0, ∞}`.

The value `r = 0` is not allowed because we want dilations of (e)metric spaces to be automatically injective. The value `r = ∞` is not allowed because this way we can define `Dilation.ratio f : ℝ≥0`, not `Dilation.ratio f : ℝ≥0∞`. Also, we do not often need maps sending distinct points to points at infinite distance.

## Main definitions #

- `Dilation.ratio f : ℝ≥0`: the value of `r` in the relation above, defaulting to 1 in the case where it is not well-defined.

## Notation #

- `α →ᵈ β`: notation for `Dilation α β`.

## Implementation notes #

The type of dilations defined in this file are also referred to as "similarities" or "similitudes" by other authors. The name `Dilation` was chosen to match the Wikipedia name.

Since a lot of elementary properties don't require `eq_of_dist_eq_zero` we start setting up the theory for `PseudoEMetricSpace` and we specialize to `PseudoMetricSpace` and `MetricSpace` when needed.

## TODO #

- Introduce dilation equivs.
- Refactor the `Isometry` API to match the `*HomClass` API below.

## References #

- https://en.wikipedia.org/wiki/Dilation_(metric_space)
- [Marcel Berger, Geometry][berger1987]

source
structure Dilation (α : Type u_1) (β : Type u_2) [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
Type (max u_1 u_2)

A dilation is a map that uniformly scales the edistance between any two points.

- toFun : α → β

  The underlying function.

  Do NOT use directly. Use the coercion instead.

- edist_eq' : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (self.toFun x) (self.toFun y) = ↑r * edist x y

Instances For

source
def «term_→ᵈ_» :
Lean.TrailingParserDescr

A dilation is a map that uniformly scales the edistance between any two points.

Equations

- «term_→ᵈ_» = Lean.ParserDescr.trailingNode `«term_→ᵈ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᵈ ") (Lean.ParserDescr.cat `term 26))

Instances For

source
class DilationClass (F : Type u_3) (α : outParam (Type u_4)) (β : outParam (Type u_5)) [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] :
Prop

`DilationClass F α β r` states that `F` is a type of `r`-dilations. You should extend this typeclass when you extend `Dilation`.

- edist_eq' (f : F) : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y

Instances

source
instance Dilation.funLike {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
FunLike (α →ᵈ β) α β
Equations

- Dilation.funLike = { coe := Dilation.toFun, coe_injective' := ⋯ }

source
instance Dilation.toDilationClass {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
DilationClass (α →ᵈ β) α β
source
@[simp]
theorem Dilation.toFun_eq_coe {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α →ᵈ β} :
f.toFun = ⇑f
source
@[simp]
theorem Dilation.coe_mk {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y) :
⇑{ toFun := f, edist_eq' := h } = f
source
theorem Dilation.congr_fun {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f g : α →ᵈ β} (h : f = g) (x : α) :
f x = g x
source
theorem Dilation.congr_arg {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) {x y : α} (h : x = y) :
f x = f y
source
theorem Dilation.ext {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f g : α →ᵈ β} (h : ∀ (x : α), f x = g x) :
f = g
source
theorem Dilation.ext_iff {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f g : α →ᵈ β} :
f = g ↔ ∀ (x : α), f x = g x
source
@[simp]
theorem Dilation.mk_coe {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y) :
{ toFun := ⇑f, edist_eq' := h } = f
source
def Dilation.copy {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) (f' : α → β) (h : f' = ⇑f) :
α →ᵈ β

Copy of a `Dilation` with a new `toFun` equal to the old one. Useful to fix definitional equalities.

Equations

- f.copy f' h = { toFun := f', edist_eq' := ⋯ }

Instances For

source
@[simp]
theorem Dilation.copy_toFun {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) (f' : α → β) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem Dilation.copy_eq_self {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) {f' : α → β} (h : f' = ⇑f) :
f.copy f' h = f
source
def Dilation.ratio {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
NNReal

The ratio of a dilation `f`. If the ratio is undefined (i.e., the distance between any two points in `α` is either zero or infinity), then we choose one as the ratio.

Equations

- Dilation.ratio f = if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1 else ⋯.choose

Instances For

source
theorem Dilation.ratio_of_trivial {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤) :
ratio f = 1
source
theorem Dilation.ratio_of_subsingleton {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [Subsingleton α] [DilationClass F α β] (f : F) :
ratio f = 1
source
theorem Dilation.ratio_ne_zero {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
ratio f ≠ 0
source
theorem Dilation.ratio_pos {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
0 < ratio f
source
@[simp]
theorem Dilation.edist_eq {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x y : α) :
edist (f x) (f y) = ↑(ratio f) * edist x y
source
@[simp]
theorem Dilation.nndist_eq {α : Type u_5} {β : Type u_6} {F : Type u_7} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x y : α) :
nndist (f x) (f y) = ratio f * nndist x y
source
@[simp]
theorem Dilation.dist_eq {α : Type u_5} {β : Type u_6} {F : Type u_7} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x y : α) :
dist (f x) (f y) = ↑(ratio f) * dist x y
source
theorem Dilation.ratio_unique {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] {f : F} {x y : α} {r : NNReal} (h₀ : edist x y ≠ 0) (htop : edist x y ≠ ⊤) (hr : edist (f x) (f y) = ↑r * edist x y) :
r = ratio f

The `ratio` is equal to the distance ratio for any two points with nonzero finite distance. `dist` and `nndist` versions below

source
theorem Dilation.ratio_unique_of_nndist_ne_zero {α : Type u_5} {β : Type u_6} {F : Type u_7} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] {f : F} {x y : α} {r : NNReal} (hxy : nndist x y ≠ 0) (hr : nndist (f x) (f y) = r * nndist x y) :
r = ratio f

The `ratio` is equal to the distance ratio for any two points with nonzero finite distance; `nndist` version

source
theorem Dilation.ratio_unique_of_dist_ne_zero {α : Type u_6} {β : Type u_7} {F : Type u_5} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] {f : F} {x y : α} {r : NNReal} (hxy : dist x y ≠ 0) (hr : dist (f x) (f y) = ↑r * dist x y) :
r = ratio f

The `ratio` is equal to the distance ratio for any two points with nonzero finite distance; `dist` version

source
def Dilation.mkOfNNDistEq {α : Type u_5} {β : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) :
α →ᵈ β

Alternative `Dilation` constructor when the distance hypothesis is over `nndist`

Equations

- Dilation.mkOfNNDistEq f h = { toFun := f, edist_eq' := ⋯ }

Instances For

source
@[simp]
theorem Dilation.coe_mkOfNNDistEq {α : Type u_5} {β : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) :
⇑(mkOfNNDistEq f h) = f
source
@[simp]
theorem Dilation.mk_coe_of_nndist_eq {α : Type u_5} {β : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α →ᵈ β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) :
mkOfNNDistEq (⇑f) h = f
source
def Dilation.mkOfDistEq {α : Type u_5} {β : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y) :
α →ᵈ β

Alternative `Dilation` constructor when the distance hypothesis is over `dist`

Equations

- Dilation.mkOfDistEq f h = Dilation.mkOfNNDistEq f ⋯

Instances For

source
@[simp]
theorem Dilation.coe_mkOfDistEq {α : Type u_5} {β : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y) :
⇑(mkOfDistEq f h) = f
source
@[simp]
theorem Dilation.mk_coe_of_dist_eq {α : Type u_5} {β : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α →ᵈ β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y) :
mkOfDistEq (⇑f) h = f
source
def Isometry.toDilation {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) (hf : Isometry f) :
α →ᵈ β

Every isometry is a dilation of ratio `1`.

Equations

- Isometry.toDilation f hf = { toFun := f, edist_eq' := ⋯ }

Instances For

source
@[simp]
theorem Isometry.toDilation_toFun {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) (hf : Isometry f) (a✝ : α) :
(toDilation f hf) a✝ = f a✝
source
@[simp]
theorem Isometry.toDilation_ratio {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {hf : Isometry f} :
Dilation.ratio (toDilation f hf) = 1
source
theorem Dilation.lipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
LipschitzWith (ratio f) ⇑f
source
theorem Dilation.antilipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
AntilipschitzWith (ratio f)⁻¹ ⇑f
source
theorem Dilation.injective {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace β] {α : Type u_5} [EMetricSpace α] [FunLike F α β] [DilationClass F α β] (f : F) :
Function.Injective ⇑f

A dilation from an emetric space is injective

source
def Dilation.id (α : Type u_5) [PseudoEMetricSpace α] :
α →ᵈ α

The identity is a dilation

Equations

- Dilation.id α = { toFun := id, edist_eq' := ⋯ }

Instances For

source
instance Dilation.instInhabited {α : Type u_1} [PseudoEMetricSpace α] :
Inhabited (α →ᵈ α)
Equations

- Dilation.instInhabited = { default := Dilation.id α }

source
@[simp]
theorem Dilation.coe_id {α : Type u_1} [PseudoEMetricSpace α] :
⇑(Dilation.id α) = id
source
theorem Dilation.ratio_id {α : Type u_1} [PseudoEMetricSpace α] :
ratio (Dilation.id α) = 1
source
def Dilation.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (g : β →ᵈ γ) (f : α →ᵈ β) :
α →ᵈ γ

The composition of dilations is a dilation

Equations

- g.comp f = { toFun := ⇑g ∘ ⇑f, edist_eq' := ⋯ }

Instances For

source
theorem Dilation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {δ : Type u_5} [PseudoEMetricSpace δ] (f : α →ᵈ β) (g : β →ᵈ γ) (h : γ →ᵈ δ) :
(h.comp g).comp f = h.comp (g.comp f)
source
@[simp]
theorem Dilation.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (g : β →ᵈ γ) (f : α →ᵈ β) :
⇑(g.comp f) = ⇑g ∘ ⇑f
source
theorem Dilation.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (g : β →ᵈ γ) (f : α →ᵈ β) (x : α) :
(g.comp f) x = g (f x)
source
theorem Dilation.ratio_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β} (hne : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ⊤) :
ratio (g.comp f) = ratio g * ratio f

Ratio of the composition `g.comp f` of two dilations is the product of their ratios. We assume that there exist two points in `α` at extended distance neither `0` nor `∞` because otherwise `Dilation.ratio (g.comp f) = Dilation.ratio f = 1` while `Dilation.ratio g` can be any number. This version works for most general spaces, see also `Dilation.ratio_comp` for a version assuming that `α` is a nontrivial metric space.

source
@[simp]
theorem Dilation.comp_id {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) :
f.comp (Dilation.id α) = f
source
@[simp]
theorem Dilation.id_comp {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) :
(Dilation.id β).comp f = f
source
instance Dilation.instMonoid {α : Type u_1} [PseudoEMetricSpace α] :
Monoid (α →ᵈ α)
Equations

- Dilation.instMonoid = { mul := Dilation.comp, mul_assoc := ⋯, one := Dilation.id α, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

source
theorem Dilation.one_def {α : Type u_1} [PseudoEMetricSpace α] :
1 = Dilation.id α
source
theorem Dilation.mul_def {α : Type u_1} [PseudoEMetricSpace α] (f g : α →ᵈ α) :
f * g = f.comp g
source
@[simp]
theorem Dilation.coe_one {α : Type u_1} [PseudoEMetricSpace α] :
⇑1 = id
source
@[simp]
theorem Dilation.coe_mul {α : Type u_1} [PseudoEMetricSpace α] (f g : α →ᵈ α) :
⇑(f * g) = ⇑f ∘ ⇑g
source
@[simp]
theorem Dilation.ratio_one {α : Type u_1} [PseudoEMetricSpace α] :
ratio 1 = 1
source
@[simp]
theorem Dilation.ratio_mul {α : Type u_1} [PseudoEMetricSpace α] (f g : α →ᵈ α) :
ratio (f * g) = ratio f * ratio g
source
def Dilation.ratioHom {α : Type u_1} [PseudoEMetricSpace α] :
(α →ᵈ α) →* NNReal

`Dilation.ratio` as a monoid homomorphism from `α →ᵈ α` to `ℝ≥0`.

Equations

- Dilation.ratioHom = { toFun := Dilation.ratio, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem Dilation.ratioHom_apply {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) :
ratioHom f = ratio f
source
@[simp]
theorem Dilation.ratio_pow {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) (n : ℕ) :
ratio (f ^ n) = ratio f ^ n
source
@[simp]
theorem Dilation.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g₁ g₂ : β →ᵈ γ} {f : α →ᵈ β} (hf : Function.Surjective ⇑f) :
g₁.comp f = g₂.comp f ↔ g₁ = g₂
source
@[simp]
theorem Dilation.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β →ᵈ γ} {f₁ f₂ : α →ᵈ β} (hg : Function.Injective ⇑g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
source
theorem Dilation.isUniformInducing {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
IsUniformInducing ⇑f

A dilation from a metric space is a uniform inducing map

source
theorem Dilation.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) {ι : Type u_5} {g : ι → α} {a : Filter ι} {b : α} :
Filter.Tendsto g a (nhds b) ↔ Filter.Tendsto (⇑f ∘ g) a (nhds (f b))
source
theorem Dilation.toContinuous {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
Continuous ⇑f

A dilation is continuous.

source
theorem Dilation.ediam_image {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (s : Set α) :
EMetric.diam (⇑f '' s) = ↑(ratio f) * EMetric.diam s

Dilations scale the diameter by `ratio f` in pseudoemetric spaces.

source
theorem Dilation.ediam_range {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
EMetric.diam (Set.range ⇑f) = ↑(ratio f) * EMetric.diam Set.univ

A dilation scales the diameter of the range by `ratio f`.

source
theorem Dilation.mapsTo_emetric_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x : α) (r : ENNReal) :
Set.MapsTo (⇑f) (EMetric.ball x r) (EMetric.ball (f x) (↑(ratio f) * r))

A dilation maps balls to balls and scales the radius by `ratio f`.

source
theorem Dilation.mapsTo_emetric_closedBall {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x : α) (r' : ENNReal) :
Set.MapsTo (⇑f) (EMetric.closedBall x r') (EMetric.closedBall (f x) (↑(ratio f) * r'))

A dilation maps closed balls to closed balls and scales the radius by `ratio f`.

source
theorem Dilation.comp_continuousOn_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) {γ : Type u_5} [TopologicalSpace γ] {g : γ → α} {s : Set γ} :
ContinuousOn (⇑f ∘ g) s ↔ ContinuousOn g s
source
theorem Dilation.comp_continuous_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) {γ : Type u_5} [TopologicalSpace γ] {g : γ → α} :
Continuous (⇑f ∘ g) ↔ Continuous g
source
theorem Dilation.isUniformEmbedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [EMetricSpace α] [FunLike F α β] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) :
IsUniformEmbedding ⇑f

A dilation from a metric space is a uniform embedding

source
theorem Dilation.isEmbedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [EMetricSpace α] [FunLike F α β] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) :
Topology.IsEmbedding ⇑f

A dilation from a metric space is an embedding

source
theorem Dilation.isClosedEmbedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [EMetricSpace α] [FunLike F α β] [CompleteSpace α] [EMetricSpace β] [DilationClass F α β] (f : F) :
Topology.IsClosedEmbedding ⇑f

A dilation from a complete emetric space is a closed embedding

source
@[simp]
theorem Dilation.ratio_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MetricSpace α] [Nontrivial α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β} :
ratio (g.comp f) = ratio g * ratio f

Ratio of the composition `g.comp f` of two dilations is the product of their ratios. We assume that the domain `α` of `f` is a nontrivial metric space, otherwise `Dilation.ratio f = Dilation.ratio (g.comp f) = 1` but `Dilation.ratio g` may have any value.

See also `Dilation.ratio_comp'` for a version that works for more general spaces.

source
theorem Dilation.diam_image {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (s : Set α) :
Metric.diam (⇑f '' s) = ↑(ratio f) * Metric.diam s

A dilation scales the diameter by `ratio f` in pseudometric spaces.

source
theorem Dilation.diam_range {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
Metric.diam (Set.range ⇑f) = ↑(ratio f) * Metric.diam Set.univ
source
theorem Dilation.mapsTo_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x : α) (r' : ℝ) :
Set.MapsTo (⇑f) (Metric.ball x r') (Metric.ball (f x) (↑(ratio f) * r'))

A dilation maps balls to balls and scales the radius by `ratio f`.

source
theorem Dilation.mapsTo_sphere {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x : α) (r' : ℝ) :
Set.MapsTo (⇑f) (Metric.sphere x r') (Metric.sphere (f x) (↑(ratio f) * r'))

A dilation maps spheres to spheres and scales the radius by `ratio f`.

source
theorem Dilation.mapsTo_closedBall {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x : α) (r' : ℝ) :
Set.MapsTo (⇑f) (Metric.closedBall x r') (Metric.closedBall (f x) (↑(ratio f) * r'))

A dilation maps closed balls to closed balls and scales the radius by `ratio f`.

source
theorem Dilation.tendsto_cobounded {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
Filter.Tendsto (⇑f) (Bornology.cobounded α) (Bornology.cobounded β)
source
@[simp]
theorem Dilation.comap_cobounded {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
Filter.comap (⇑f) (Bornology.cobounded β) = Bornology.cobounded α