Product of pseudo-metric spaces and other constructions

This file constructs the infinity distance on finite products of normed groups 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 Inducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : α → β} (hf : Inducing 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 ⋯

def UniformInducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [UniformSpace α] [m : PseudoMetricSpace β] (f : α → β) (h : UniformInducing 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

• UniformInducing.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 : Subtype p) (y : Subtype p) : dist x y = dist ↑x ↑y

theorem Subtype.nndist_eq {α : Type u_1} [PseudoMetricSpace α] {p : α → Prop} (x : Subtype p) (y : Subtype p) : nndist x y = nndist ↑x ↑y

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

Equations

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

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

Equations

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

@[simp]

theorem AddOpposite.dist_unop {α : Type u_1} [PseudoMetricSpace α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : dist (AddOpposite.unop x) (AddOpposite.unop y) = dist x y

@[simp]

theorem MulOpposite.dist_unop {α : Type u_1} [PseudoMetricSpace α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : dist (MulOpposite.unop x) (MulOpposite.unop y) = dist x y

@[simp]

theorem AddOpposite.dist_op {α : Type u_1} [PseudoMetricSpace α] (x : α) (y : α) : dist (AddOpposite.op x) (AddOpposite.op y) = dist x y

@[simp]

theorem MulOpposite.dist_op {α : Type u_1} [PseudoMetricSpace α] (x : α) (y : α) : dist (MulOpposite.op x) (MulOpposite.op y) = dist x y

@[simp]

theorem AddOpposite.nndist_unop {α : Type u_1} [PseudoMetricSpace α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : nndist (AddOpposite.unop x) (AddOpposite.unop y) = nndist x y

@[simp]

theorem MulOpposite.nndist_unop {α : Type u_1} [PseudoMetricSpace α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : nndist (MulOpposite.unop x) (MulOpposite.unop y) = nndist x y

@[simp]

theorem AddOpposite.nndist_op {α : Type u_1} [PseudoMetricSpace α] (x : α) (y : α) : nndist (AddOpposite.op x) (AddOpposite.op y) = nndist x y

@[simp]

theorem MulOpposite.nndist_op {α : Type u_1} [PseudoMetricSpace α] (x : α) (y : α) : nndist (MulOpposite.op x) (MulOpposite.op y) = nndist x y

instance instPseudoMetricSpaceNNReal : PseudoMetricSpace NNReal

Equations

• instPseudoMetricSpaceNNReal = Subtype.pseudoMetricSpace

theorem NNReal.dist_eq (a : NNReal) (b : NNReal) : dist a b = |↑a - ↑b|

theorem NNReal.nndist_eq (a : NNReal) (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 : NNReal) (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 : ULift.{u_3, u_2} β) (y : ULift.{u_3, u_2} β) : dist x y = dist x.down y.down

theorem ULift.nndist_eq {β : Type u_2} [PseudoMetricSpace β] (x : ULift.{u_3, u_2} β) (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 = let i := PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (x y : α × β) => dist x.1 y.1 ⊔ dist x.2 y.2) ⋯ ⋯; i.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 : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.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 : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.Tendsto (fun (x : β) => nndist (f x) (g x)) x (nhds (nndist a b))

instance pseudoMetricSpacePi {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] : PseudoMetricSpace ((b : β) → π b)

A finite product of pseudometric spaces is a pseudometric space, with the sup distance.

Equations

• pseudoMetricSpacePi = let i := PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (f g : (b : β) → π b) => ↑(Finset.univ.sup fun (b : β) => nndist (f b) (g b))) ⋯ ⋯; i.replaceBornology ⋯

theorem nndist_pi_def {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) : nndist f g = Finset.univ.sup fun (b : β) => nndist (f b) (g b)

theorem dist_pi_def {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) : dist f g = ↑(Finset.univ.sup fun (b : β) => nndist (f b) (g b))

theorem nndist_pi_le_iff {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} : nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r

theorem nndist_pi_lt_iff {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} (hr : 0 < r) : nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r

theorem nndist_pi_eq_iff {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} (hr : 0 < r) : nndist f g = r ↔ (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

theorem dist_pi_lt_iff {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : ℝ} (hr : 0 < r) : dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r

theorem dist_pi_le_iff {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : ℝ} (hr : 0 ≤ r) : dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_eq_iff {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : ℝ} (hr : 0 < r) : dist f g = r ↔ (∃ (i : β), dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_le_iff' {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] {f : (b : β) → π b} {g : (b : β) → π b} {r : ℝ} : dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_const_le {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [Fintype β] (a : α) (b : α) : (dist (fun (x : β) => a) fun (x : β) => b) ≤ dist a b

theorem nndist_pi_const_le {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [Fintype β] (a : α) (b : α) : (nndist (fun (x : β) => a) fun (x : β) => b) ≤ nndist a b

@[simp]

theorem dist_pi_const {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [Fintype β] [Nonempty β] (a : α) (b : α) : (dist (fun (x : β) => a) fun (x : β) => b) = dist a b

@[simp]

theorem nndist_pi_const {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [Fintype β] [Nonempty β] (a : α) (b : α) : (nndist (fun (x : β) => a) fun (x : β) => b) = nndist a b

theorem nndist_le_pi_nndist {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) (b : β) : nndist (f b) (g b) ≤ nndist f g

theorem dist_le_pi_dist {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) (b : β) : dist (f b) (g b) ≤ dist f g

theorem ball_pi {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ} (hr : 0 < r) : Metric.ball x r = Set.univ.pi fun (b : β) => Metric.ball (x b) r

An open ball in a product space is a product of open balls. See also ball_pi' for a version assuming Nonempty β instead of 0 < r.

theorem ball_pi' {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] (x : (b : β) → π b) (r : ℝ) : Metric.ball x r = Set.univ.pi fun (b : β) => Metric.ball (x b) r

An open ball in a product space is a product of open balls. See also ball_pi for a version assuming 0 < r instead of Nonempty β.

theorem closedBall_pi {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ} (hr : 0 ≤ r) : Metric.closedBall x r = Set.univ.pi fun (b : β) => Metric.closedBall (x b) r

A closed ball in a product space is a product of closed balls. See also closedBall_pi' for a version assuming Nonempty β instead of 0 ≤ r.

theorem closedBall_pi' {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] (x : (b : β) → π b) (r : ℝ) : Metric.closedBall x r = Set.univ.pi fun (b : β) => Metric.closedBall (x b) r

A closed ball in a product space is a product of closed balls. See also closedBall_pi for a version assuming 0 ≤ r instead of Nonempty β.

theorem sphere_pi {β : Type u_2} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ} (h : 0 < r ∨ Nonempty β) : Metric.sphere x r = (⋃ (i : β), Function.eval i ⁻¹' Metric.sphere (x i) r) ∩ Metric.closedBall x r

A sphere in a product space is a union of spheres on each component restricted to the closed ball.

@[simp]

theorem Fin.nndist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x : α i) (y : α i) (f : (j : Fin n) → α (i.succAbove j)) (g : (j : Fin n) → α (i.succAbove j)) : nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g)

@[simp]

theorem Fin.dist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x : α i) (y : α i) (f : (j : Fin n) → α (i.succAbove j)) (g : (j : Fin n) → α (i.succAbove j)) : dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)

instance instPseudoMetricSpaceAdditive {α : Type u_1} [PseudoMetricSpace α] : PseudoMetricSpace (Additive α)

Equations

• instPseudoMetricSpaceAdditive = inst

instance instPseudoMetricSpaceMultiplicative {α : Type u_1} [PseudoMetricSpace α] : PseudoMetricSpace (Multiplicative α)

Equations

• instPseudoMetricSpaceMultiplicative = inst

instance instPseudoMetricSpaceOrderDual {α : Type u_1} [PseudoMetricSpace α] : PseudoMetricSpace αᵒᵈ

Equations

• instPseudoMetricSpaceOrderDual = inst