Documentation

Mathlib.Topology.MetricSpace.Pseudo.Constructions

Products of pseudometric spaces and other constructions #

This file constructs the supremum distance on binary products of pseudometric spaces and provides instances for type synonyms.

@[reducible, inline]
abbrev PseudoMetricSpace.induced {α : Type u_3} {β : Type u_4} (f : αβ) (m : PseudoMetricSpace β) :

Pseudometric space structure pulled back by a function.

Equations
  • One or more equations did not get rendered due to their size.
def Topology.IsInducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : αβ} (hf : IsInducing f) :

Pull back a pseudometric space structure by an inducing map. This is a version of PseudoMetricSpace.induced useful in case if the domain already has a TopologicalSpace structure.

Equations
@[deprecated Topology.IsInducing.comapPseudoMetricSpace (since := "2024-10-28")]
def Inducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : αβ} (hf : Topology.IsInducing f) :

Alias of Topology.IsInducing.comapPseudoMetricSpace.


Pull back a pseudometric space structure by an inducing map. This is a version of PseudoMetricSpace.induced useful in case if the domain already has a TopologicalSpace structure.

Equations
def IsUniformInducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [UniformSpace α] [m : PseudoMetricSpace β] (f : αβ) (h : IsUniformInducing f) :

Pull back a pseudometric space structure by a uniform inducing map. This is a version of PseudoMetricSpace.induced useful in case if the domain already has a UniformSpace structure.

Equations
theorem Subtype.dist_eq {α : Type u_1} [PseudoMetricSpace α] {p : αProp} (x y : Subtype p) :
dist x y = dist x y
theorem Subtype.nndist_eq {α : Type u_1} [PseudoMetricSpace α] {p : αProp} (x y : Subtype p) :
nndist x y = nndist x y
@[simp]
theorem MulOpposite.dist_unop {α : Type u_1} [PseudoMetricSpace α] (x y : αᵐᵒᵖ) :
dist (unop x) (unop y) = dist x y
@[simp]
theorem AddOpposite.dist_unop {α : Type u_1} [PseudoMetricSpace α] (x y : αᵃᵒᵖ) :
dist (unop x) (unop y) = dist x y
@[simp]
theorem MulOpposite.dist_op {α : Type u_1} [PseudoMetricSpace α] (x y : α) :
dist (op x) (op y) = dist x y
@[simp]
theorem AddOpposite.dist_op {α : Type u_1} [PseudoMetricSpace α] (x y : α) :
dist (op x) (op y) = dist x y
@[simp]
theorem MulOpposite.nndist_unop {α : Type u_1} [PseudoMetricSpace α] (x y : αᵐᵒᵖ) :
nndist (unop x) (unop y) = nndist x y
@[simp]
theorem AddOpposite.nndist_unop {α : Type u_1} [PseudoMetricSpace α] (x y : αᵃᵒᵖ) :
nndist (unop x) (unop y) = nndist x y
@[simp]
theorem MulOpposite.nndist_op {α : Type u_1} [PseudoMetricSpace α] (x y : α) :
nndist (op x) (op y) = nndist x y
@[simp]
theorem AddOpposite.nndist_op {α : Type u_1} [PseudoMetricSpace α] (x y : α) :
nndist (op x) (op y) = nndist x y
theorem NNReal.dist_eq (a b : NNReal) :
dist a b = |a - b|
theorem NNReal.nndist_eq (a b : NNReal) :
nndist a b = max (a - b) (b - a)
@[simp]
@[simp]
theorem NNReal.le_add_nndist (a b : NNReal) :
a b + nndist a b
theorem ULift.dist_eq {β : Type u_2} [PseudoMetricSpace β] (x y : ULift.{u_3, u_2} β) :
dist x y = dist x.down y.down
@[simp]
theorem ULift.dist_up_up {β : Type u_2} [PseudoMetricSpace β] (x y : β) :
dist { down := x } { down := y } = dist x y
@[simp]
theorem ULift.nndist_up_up {β : Type u_2} [PseudoMetricSpace β] (x y : β) :
nndist { down := x } { down := y } = nndist x y
Equations
theorem Prod.dist_eq {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] {x y : α × β} :
dist x y = max (dist x.1 y.1) (dist x.2 y.2)
@[simp]
theorem dist_prod_same_left {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] {x : α} {y₁ y₂ : β} :
dist (x, y₁) (x, y₂) = dist y₁ y₂
@[simp]
theorem dist_prod_same_right {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] {x₁ x₂ : α} {y : β} :
dist (x₁, y) (x₂, y) = dist x₁ x₂
theorem ball_prod_same {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ) :
theorem closedBall_prod_same {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ) :
theorem sphere_prod {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α × β) (r : ) :
theorem uniformContinuous_dist {α : Type u_1} [PseudoMetricSpace α] :
UniformContinuous fun (p : α × α) => dist p.1 p.2
theorem UniformContinuous.dist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [UniformSpace β] {f g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
UniformContinuous fun (b : β) => dist (f b) (g b)
theorem continuous_dist {α : Type u_1} [PseudoMetricSpace α] :
Continuous fun (p : α × α) => dist p.1 p.2
theorem Continuous.dist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [TopologicalSpace β] {f g : βα} (hf : Continuous f) (hg : Continuous g) :
Continuous fun (b : β) => dist (f b) (g b)
theorem Filter.Tendsto.dist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {f g : βα} {x : Filter β} {a b : α} (hf : Tendsto f x (nhds a)) (hg : Tendsto g x (nhds b)) :
Tendsto (fun (x : β) => dist (f x) (g x)) x (nhds (dist a b))
theorem continuous_iff_continuous_dist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [TopologicalSpace β] {f : βα} :
Continuous f Continuous fun (x : β × β) => dist (f x.1) (f x.2)
theorem uniformContinuous_nndist {α : Type u_1} [PseudoMetricSpace α] :
UniformContinuous fun (p : α × α) => nndist p.1 p.2
theorem UniformContinuous.nndist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [UniformSpace β] {f g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
UniformContinuous fun (b : β) => nndist (f b) (g b)
theorem continuous_nndist {α : Type u_1} [PseudoMetricSpace α] :
Continuous fun (p : α × α) => nndist p.1 p.2
theorem Continuous.nndist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [TopologicalSpace β] {f g : βα} (hf : Continuous f) (hg : Continuous g) :
Continuous fun (b : β) => nndist (f b) (g b)
theorem Filter.Tendsto.nndist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {f g : βα} {x : Filter β} {a b : α} (hf : Tendsto f x (nhds a)) (hg : Tendsto g x (nhds b)) :
Tendsto (fun (x : β) => nndist (f x) (g x)) x (nhds (nndist a b))