Documentation

Mathlib.Topology.MetricSpace.Pseudo.Pi

Product of pseudometric spaces #

This file constructs the infinity distance on finite products of pseudometric spaces.

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
    theorem nndist_pi_def {β : Type u_2} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f 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 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 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 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 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 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 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 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 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 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 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 β) :

    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 y : α i) (f 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 y : α i) (f g : (j : Fin n) → α (i.succAbove j)) :
    dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)