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.
Instances For
def
Inducing.comapPseudoMetricSpace
{α : Type u_3}
{β : Type u_4}
[TopologicalSpace α]
[m : PseudoMetricSpace β]
{f : α → β}
(hf : Inducing 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
- hf.comapPseudoMetricSpace = (PseudoMetricSpace.induced f m).replaceTopology ⋯
Instances For
def
UniformInducing.comapPseudoMetricSpace
{α : Type u_3}
{β : Type u_4}
[UniformSpace α]
[m : PseudoMetricSpace β]
(f : α → β)
(h : UniformInducing 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
- UniformInducing.comapPseudoMetricSpace f h = (PseudoMetricSpace.induced f m).replaceUniformity ⋯
Instances For
Equations
- Subtype.pseudoMetricSpace = PseudoMetricSpace.induced Subtype.val inst
theorem
Subtype.dist_eq
{α : Type u_1}
[PseudoMetricSpace α]
{p : α → Prop}
(x : Subtype p)
(y : Subtype p)
:
theorem
Subtype.nndist_eq
{α : Type u_1}
[PseudoMetricSpace α]
{p : α → Prop}
(x : Subtype p)
(y : Subtype p)
:
Equations
- AddOpposite.instPseudoMetricSpace = PseudoMetricSpace.induced AddOpposite.unop inst
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
Equations
- instPseudoMetricSpaceNNReal = Subtype.pseudoMetricSpace
theorem
NNReal.closedBall_zero_eq_Icc
{c : ℝ}
(c_nn : 0 ≤ c)
:
Metric.closedBall 0 c = Set.Icc 0 c.toNNReal
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} β)
:
theorem
ULift.nndist_eq
{β : Type u_2}
[PseudoMetricSpace β]
(x : ULift.{u_3, u_2} β)
(y : ULift.{u_3, u_2} β)
:
@[simp]
@[simp]
instance
Prod.pseudoMetricSpaceMax
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
:
PseudoMetricSpace (α × β)
theorem
Prod.dist_eq
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{x : α × β}
{y : α × β}
:
@[simp]
theorem
dist_prod_same_left
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{x : α}
{y₁ : β}
{y₂ : β}
:
@[simp]
theorem
dist_prod_same_right
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{x₁ : α}
{x₂ : α}
{y : β}
:
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))