# 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.

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

Pseudometric space structure pulled back by a function.

Equations

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

Instances For

source
def Topology.IsInducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : α → β} (hf : IsInducing f) :
PseudoMetricSpace α

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

- hf.comapPseudoMetricSpace = (PseudoMetricSpace.induced f m).replaceTopology ⋯

Instances For

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

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

- IsUniformInducing.comapPseudoMetricSpace f h = (PseudoMetricSpace.induced f m).replaceUniformity ⋯

Instances For

source
instance Subtype.pseudoMetricSpace {α : Type u_1} [PseudoMetricSpace α] {p : α → Prop} :
PseudoMetricSpace (Subtype p)
Equations

- Subtype.pseudoMetricSpace = PseudoMetricSpace.induced Subtype.val inst✝

source
theorem Subtype.dist_eq {α : Type u_1} [PseudoMetricSpace α] {p : α → Prop} (x y : Subtype p) :
dist x y = dist ↑x ↑y
source
theorem Subtype.nndist_eq {α : Type u_1} [PseudoMetricSpace α] {p : α → Prop} (x y : Subtype p) :
nndist x y = nndist ↑x ↑y
source
instance MulOpposite.instPseudoMetricSpace {α : Type u_1} [PseudoMetricSpace α] :
PseudoMetricSpace α ᵐᵒᵖ
Equations

- MulOpposite.instPseudoMetricSpace = PseudoMetricSpace.induced MulOpposite.unop inst✝

source
instance AddOpposite.instPseudoMetricSpace {α : Type u_1} [PseudoMetricSpace α] :
PseudoMetricSpace α ᵃᵒᵖ
Equations

- AddOpposite.instPseudoMetricSpace = PseudoMetricSpace.induced AddOpposite.unop inst✝

source
@[simp]
theorem MulOpposite.dist_unop {α : Type u_1} [PseudoMetricSpace α] (x y : α ᵐᵒᵖ) :
dist (unop x) (unop y) = dist x y
source
@[simp]
theorem AddOpposite.dist_unop {α : Type u_1} [PseudoMetricSpace α] (x y : α ᵃᵒᵖ) :
dist (unop x) (unop y) = dist x y
source
@[simp]
theorem MulOpposite.dist_op {α : Type u_1} [PseudoMetricSpace α] (x y : α) :
dist (op x) (op y) = dist x y
source
@[simp]
theorem AddOpposite.dist_op {α : Type u_1} [PseudoMetricSpace α] (x y : α) :
dist (op x) (op y) = dist x y
source
@[simp]
theorem MulOpposite.nndist_unop {α : Type u_1} [PseudoMetricSpace α] (x y : α ᵐᵒᵖ) :
nndist (unop x) (unop y) = nndist x y
source
@[simp]
theorem AddOpposite.nndist_unop {α : Type u_1} [PseudoMetricSpace α] (x y : α ᵃᵒᵖ) :
nndist (unop x) (unop y) = nndist x y
source
@[simp]
theorem MulOpposite.nndist_op {α : Type u_1} [PseudoMetricSpace α] (x y : α) :
nndist (op x) (op y) = nndist x y
source
@[simp]
theorem AddOpposite.nndist_op {α : Type u_1} [PseudoMetricSpace α] (x y : α) :
nndist (op x) (op y) = nndist x y
source
instance instPseudoMetricSpaceNNReal :
PseudoMetricSpace NNReal
Equations

- instPseudoMetricSpaceNNReal = Subtype.pseudoMetricSpace

source
theorem NNReal.dist_eq (a b : NNReal) :
dist a b = |↑a - ↑b|
source
theorem NNReal.nndist_eq (a b : NNReal) :
nndist a b = max (a - b) (b - a)
source
@[simp]
theorem NNReal.nndist_zero_eq_val (z : NNReal) :
nndist 0 z = z
source
@[simp]
theorem NNReal.nndist_zero_eq_val' (z : NNReal) :
nndist z 0 = z
source
theorem NNReal.le_add_nndist (a b : NNReal) :
a ≤ b + nndist a b
source
theorem NNReal.ball_zero_eq_Ico' (c : NNReal) :
Metric.ball 0 ↑c = Set.Ico 0 c
source
theorem NNReal.ball_zero_eq_Ico (c : ℝ) :
Metric.ball 0 c = Set.Ico 0 c.toNNReal
source
theorem NNReal.closedBall_zero_eq_Icc' (c : NNReal) :
Metric.closedBall 0 ↑c = Set.Icc 0 c
source
theorem NNReal.closedBall_zero_eq_Icc {c : ℝ} (c_nn : 0 ≤ c) :
Metric.closedBall 0 c = Set.Icc 0 c.toNNReal
source
instance ULift.instPseudoMetricSpace {β : Type u_2} [PseudoMetricSpace β] :
PseudoMetricSpace (ULift.{u_3, u_2} β)
Equations

- ULift.instPseudoMetricSpace = PseudoMetricSpace.induced ULift.down inst✝

source
theorem ULift.dist_eq {β : Type u_2} [PseudoMetricSpace β] (x y : ULift.{u_3, u_2} β) :
dist x y = dist x.down y.down
source
theorem ULift.nndist_eq {β : Type u_2} [PseudoMetricSpace β] (x y : ULift.{u_3, u_2} β) :
nndist x y = nndist x.down y.down
source
@[simp]
theorem ULift.dist_up_up {β : Type u_2} [PseudoMetricSpace β] (x y : β) :
dist { down := x } { down := y } = dist x y
source
@[simp]
theorem ULift.nndist_up_up {β : Type u_2} [PseudoMetricSpace β] (x y : β) :
nndist { down := x } { down := y } = nndist x y
source
instance Prod.pseudoMetricSpaceMax {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] :
PseudoMetricSpace (α × β)
Equations

- Prod.pseudoMetricSpaceMax = (PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (x y : α × β) => max (dist x.1 y.1) (dist x.2 y.2)) ⋯ ⋯).replaceBornology ⋯

source
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)
source
@[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₂
source
@[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₂
source
theorem ball_prod_same {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ℝ) :
Metric.ball x r ×ˢ Metric.ball y r = Metric.ball (x, y) r
source
theorem closedBall_prod_same {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ℝ) :
Metric.closedBall x r ×ˢ Metric.closedBall y r = Metric.closedBall (x, y) r
source
theorem sphere_prod {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α × β) (r : ℝ) :
Metric.sphere x r = Metric.sphere x.1 r ×ˢ Metric.closedBall x.2 r ∪ Metric.closedBall x.1 r ×ˢ Metric.sphere x.2 r
source
theorem uniformContinuous_dist {α : Type u_1} [PseudoMetricSpace α] :
UniformContinuous fun (p : α × α) => dist p.1 p.2
source
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)
source
theorem continuous_dist {α : Type u_1} [PseudoMetricSpace α] :
Continuous fun (p : α × α) => dist p.1 p.2
source
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)
source
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))
source
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)
source
theorem uniformContinuous_nndist {α : Type u_1} [PseudoMetricSpace α] :
UniformContinuous fun (p : α × α) => nndist p.1 p.2
source
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)
source
theorem continuous_nndist {α : Type u_1} [PseudoMetricSpace α] :
Continuous fun (p : α × α) => nndist p.1 p.2
source
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)
source
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))