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 β) : 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) : 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 ⋯

@[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) : PseudoMetricSpace α

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

• @Inducing.comapPseudoMetricSpace = @Topology.IsInducing.comapPseudoMetricSpace

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 ⋯

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

Equations

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

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

instance MulOpposite.instPseudoMetricSpace {α : Type u_1} [PseudoMetricSpace α] : PseudoMetricSpace αᵐᵒᵖ

Equations

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

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

Equations

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

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

instance instPseudoMetricSpaceNNReal : PseudoMetricSpace NNReal

Equations

• instPseudoMetricSpaceNNReal = Subtype.pseudoMetricSpace

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]

theorem NNReal.nndist_zero_eq_val (z : NNReal) : nndist 0 z = z

@[simp]

theorem NNReal.nndist_zero_eq_val' (z : NNReal) : nndist z 0 = z

theorem NNReal.le_add_nndist (a b : NNReal) : a ≤ b + nndist a b

theorem NNReal.ball_zero_eq_Ico' (c : NNReal) : Metric.ball 0 ↑c = Set.Ico 0 c

theorem NNReal.ball_zero_eq_Ico (c : ℝ) : Metric.ball 0 c = Set.Ico 0 c.toNNReal

theorem NNReal.closedBall_zero_eq_Icc' (c : NNReal) : Metric.closedBall 0 ↑c = Set.Icc 0 c

theorem NNReal.closedBall_zero_eq_Icc {c : ℝ} (c_nn : 0 ≤ c) : Metric.closedBall 0 c = Set.Icc 0 c.toNNReal

instance ULift.instPseudoMetricSpace {β : Type u_2} [PseudoMetricSpace β] : PseudoMetricSpace (ULift.{u_3, u_2} β)

Equations

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

theorem ULift.dist_eq {β : Type u_2} [PseudoMetricSpace β] (x y : ULift.{u_3, u_2} β) : dist x y = dist x.down y.down

theorem ULift.nndist_eq {β : Type u_2} [PseudoMetricSpace β] (x y : ULift.{u_3, u_2} β) : nndist x y = nndist 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

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 ⋯

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 : ℝ) : Metric.ball x r ×ˢ Metric.ball y r = Metric.ball (x, y) r

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

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

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))