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
    Instances For
      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
        Instances For
          @[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
            Instances For
              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
                Instances For
                  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))