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 defintions

• 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 choosen 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]

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 : α → β
• edist_eq' : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (Dilation.toFun s x) (Dilation.toFun s y) = ↑r * edist x y

def «term_→ᵈ_» : Lean.TrailingParserDescr

Equations

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

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

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

• coe : F → α → β
• coe_injective' : Function.Injective FunLike.coe
• edist_eq' : ∀ (f : F), ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y

instance Dilation.toDilationClass {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : DilationClass (α →ᵈ β) α β

Equations

• Dilation.toDilationClass = DilationClass.mk (_ : ∀ (f : α →ᵈ β), ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (Dilation.toFun f x) (Dilation.toFun f y) = ↑r * edist x y)

instance Dilation.instCoeFunDilationForAll {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : CoeFun (α →ᵈ β) fun (x : α →ᵈ β) => α → β

Equations

• Dilation.instCoeFunDilationForAll = FunLike.hasCoeToFun

@[simp]

theorem Dilation.toFun_eq_coe {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α →ᵈ β} : f.toFun = ⇑f

@[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

theorem Dilation.congr_fun {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α →ᵈ β} {g : α →ᵈ β} (h : f = g) (x : α) : f x = g x

theorem Dilation.congr_arg {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) {x : α} {y : α} (h : x = y) : f x = f y

theorem Dilation.ext {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α →ᵈ β} {g : α →ᵈ β} (h : ∀ (x : α), f x = g x) : f = g

theorem Dilation.ext_iff {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α →ᵈ β} {g : α →ᵈ β} : f = g ↔ ∀ (x : α), f x = g x

@[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

@[simp]

theorem Dilation.copy_toFun {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) (f' : α → β) (h : f' = ⇑f) : ⇑(Dilation.copy f f' h) = f'

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

• Dilation.copy f f' h = { toFun := f', edist_eq' := (_ : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (f' x) (f' y) = ↑r * edist x y) }

theorem Dilation.copy_eq_self {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) {f' : α → β} (h : f' = ⇑f) : Dilation.copy f f' h = f

def Dilation.ratio {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [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 Exists.choose (_ : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y)

theorem Dilation.ratio_of_trivial {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤) : Dilation.ratio f = 1

theorem Dilation.ratio_of_subsingleton {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [Subsingleton α] [DilationClass F α β] (f : F) : Dilation.ratio f = 1

theorem Dilation.ratio_ne_zero {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : Dilation.ratio f ≠ 0

theorem Dilation.ratio_pos {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : 0 < Dilation.ratio f

@[simp]

theorem Dilation.edist_eq {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) (x : α) (y : α) : edist (f x) (f y) = ↑(Dilation.ratio f) * edist x y

@[simp]

theorem Dilation.nndist_eq {α : Type u_6} {β : Type u_7} {F : Type u_8} [PseudoMetricSpace α] [PseudoMetricSpace β] [DilationClass F α β] (f : F) (x : α) (y : α) : nndist (f x) (f y) = Dilation.ratio f * nndist x y

@[simp]

theorem Dilation.dist_eq {α : Type u_6} {β : Type u_7} {F : Type u_8} [PseudoMetricSpace α] [PseudoMetricSpace β] [DilationClass F α β] (f : F) (x : α) (y : α) : dist (f x) (f y) = ↑(Dilation.ratio f) * dist x y

theorem Dilation.ratio_unique {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [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 = Dilation.ratio f

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

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

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

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

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

def Dilation.mkOfNNDistEq {α : Type u_6} {β : Type u_7} [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' := (_ : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y) }

@[simp]

theorem Dilation.coe_mkOfNNDistEq {α : Type u_6} {β : Type u_7} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) : ⇑(Dilation.mkOfNNDistEq f h) = f

@[simp]

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

def Dilation.mkOfDistEq {α : Type u_6} {β : Type u_7} [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 (_ : ∃ (a : NNReal), a ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = a * nndist x y)

@[simp]

theorem Dilation.coe_mkOfDistEq {α : Type u_6} {β : Type u_7} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y) : ⇑(Dilation.mkOfDistEq f h) = f

@[simp]

theorem Dilation.mk_coe_of_dist_eq {α : Type u_6} {β : Type u_7} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α →ᵈ β) (h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y) : Dilation.mkOfDistEq (⇑f) h = f

theorem Dilation.lipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : LipschitzWith (Dilation.ratio f) ⇑f

theorem Dilation.antilipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : AntilipschitzWith (Dilation.ratio f)⁻¹ ⇑f

theorem Dilation.injective {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace β] {α : Type u_6} [EMetricSpace α] [DilationClass F α β] (f : F) : Function.Injective ⇑f

A dilation from an emetric space is injective

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

The identity is a dilation

Equations

• Dilation.id α = { toFun := id, edist_eq' := (_ : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist (id x) (id y) = ↑r * edist x y) }

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

Equations

• Dilation.instInhabitedDilation = { default := Dilation.id α }

@[simp]

theorem Dilation.coe_id {α : Type u_1} [PseudoEMetricSpace α] : ⇑(Dilation.id α) = id

theorem Dilation.ratio_id {α : Type u_1} [PseudoEMetricSpace α] : Dilation.ratio (Dilation.id α) = 1

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

• Dilation.comp g f = { toFun := ⇑g ∘ ⇑f, edist_eq' := (_ : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), edist ((⇑g ∘ ⇑f) x) ((⇑g ∘ ⇑f) y) = ↑r * edist x y) }

theorem Dilation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {δ : Type u_6} [PseudoEMetricSpace δ] (f : α →ᵈ β) (g : β →ᵈ γ) (h : γ →ᵈ δ) : Dilation.comp (Dilation.comp h g) f = Dilation.comp h (Dilation.comp g f)

@[simp]

theorem Dilation.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (g : β →ᵈ γ) (f : α →ᵈ β) : ⇑(Dilation.comp g f) = ⇑g ∘ ⇑f

theorem Dilation.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (g : β →ᵈ γ) (f : α →ᵈ β) (x : α) : (Dilation.comp g f) x = g (f x)

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 ≠ ⊤) : Dilation.ratio (Dilation.comp g f) = Dilation.ratio g * Dilation.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.

@[simp]

theorem Dilation.comp_id {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) : Dilation.comp f (Dilation.id α) = f

@[simp]

theorem Dilation.id_comp {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) : Dilation.comp (Dilation.id β) f = f

instance Dilation.instMonoidDilation {α : Type u_1} [PseudoEMetricSpace α] : Monoid (α →ᵈ α)

Equations

• Dilation.instMonoidDilation = Monoid.mk (_ : ∀ (f : α →ᵈ α), Dilation.comp (Dilation.id α) f = f) (_ : ∀ (f : α →ᵈ α), Dilation.comp f (Dilation.id α) = f) npowRec

theorem Dilation.one_def {α : Type u_1} [PseudoEMetricSpace α] : 1 = Dilation.id α

theorem Dilation.mul_def {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) (g : α →ᵈ α) : f * g = Dilation.comp f g

@[simp]

theorem Dilation.coe_one {α : Type u_1} [PseudoEMetricSpace α] : ⇑1 = id

@[simp]

theorem Dilation.coe_mul {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) (g : α →ᵈ α) : ⇑(f * g) = ⇑f ∘ ⇑g

@[simp]

theorem Dilation.ratio_one {α : Type u_1} [PseudoEMetricSpace α] : Dilation.ratio 1 = 1

@[simp]

theorem Dilation.ratio_mul {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) (g : α →ᵈ α) : Dilation.ratio (f * g) = Dilation.ratio f * Dilation.ratio g

@[simp]

theorem Dilation.ratioHom_apply {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) : Dilation.ratioHom f = Dilation.ratio f

def Dilation.ratioHom {α : Type u_1} [PseudoEMetricSpace α] : (α →ᵈ α) →* NNReal

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Dilation.ratio_pow {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) (n : ℕ) : Dilation.ratio (f ^ n) = Dilation.ratio f ^ n

@[simp]

theorem Dilation.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g₁ : β →ᵈ γ} {g₂ : β →ᵈ γ} {f : α →ᵈ β} (hf : Function.Surjective ⇑f) : Dilation.comp g₁ f = Dilation.comp g₂ f ↔ g₁ = g₂

@[simp]

theorem Dilation.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β →ᵈ γ} {f₁ : α →ᵈ β} {f₂ : α →ᵈ β} (hg : Function.Injective ⇑g) : Dilation.comp g f₁ = Dilation.comp g f₂ ↔ f₁ = f₂

theorem Dilation.uniformInducing {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : UniformInducing ⇑f

A dilation from a metric space is a uniform inducing map

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

theorem Dilation.toContinuous {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : Continuous ⇑f

A dilation is continuous.

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

Dilations scale the diameter by ratio f in pseudoemetric spaces.

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

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

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

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

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

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

theorem Dilation.comp_continuousOn_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) {γ : Type u_6} [TopologicalSpace γ] {g : γ → α} {s : Set γ} : ContinuousOn (⇑f ∘ g) s ↔ ContinuousOn g s

theorem Dilation.comp_continuous_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) {γ : Type u_6} [TopologicalSpace γ] {g : γ → α} : Continuous (⇑f ∘ g) ↔ Continuous g

theorem Dilation.uniformEmbedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [EMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : UniformEmbedding ⇑f

A dilation from a metric space is a uniform embedding

theorem Dilation.embedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [EMetricSpace α] [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : Embedding ⇑f

A dilation from a metric space is an embedding

theorem Dilation.closedEmbedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [EMetricSpace α] [CompleteSpace α] [EMetricSpace β] [DilationClass F α β] (f : F) : ClosedEmbedding ⇑f

A dilation from a complete emetric space is a closed embedding

@[simp]

theorem Dilation.ratio_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MetricSpace α] [Nontrivial α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β} : Dilation.ratio (Dilation.comp g f) = Dilation.ratio g * Dilation.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.

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

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

theorem Dilation.diam_range {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [DilationClass F α β] (f : F) : Metric.diam (Set.range ⇑f) = ↑(Dilation.ratio f) * Metric.diam Set.univ

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

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

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

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

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

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

theorem Dilation.tendsto_cobounded {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [DilationClass F α β] (f : F) : Filter.Tendsto (⇑f) (Bornology.cobounded α) (Bornology.cobounded β)

@[simp]

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