HepLean Documentation

Mathlib.Topology.EMetricSpace.Pi

Indexed product of extended metric spaces #

source
instance instEDistForall {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] :
EDist ((b : β) → π b)
Equations
  • instEDistForall = { edist := fun (f g : (b : β) → π b) => Finset.univ.sup fun (b : β) => edist (f b) (g b) }
source
theorem edist_pi_def {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] (f g : (b : β) → π b) :
edist f g = Finset.univ.sup fun (b : β) => edist (f b) (g b)
source
theorem edist_le_pi_edist {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] (f g : (b : β) → π b) (b : β) :
edist (f b) (g b) ≤ edist f g
source
theorem edist_pi_le_iff {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] {f g : (b : β) → π b} {d : ENNReal} :
edist f g ≤ d ↔ ∀ (b : β), edist (f b) (g b) ≤ d
source
theorem edist_pi_const_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Fintype β] (a b : α) :
(edist (fun (x : β) => a) fun (x : β) => b) ≤ edist a b
source
@[simp]
theorem edist_pi_const {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Fintype β] [Nonempty β] (a b : α) :
(edist (fun (x : β) => a) fun (x : β) => b) = edist a b
source
instance pseudoEMetricSpacePi {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → PseudoEMetricSpace (π b)] :
PseudoEMetricSpace ((b : β) → π b)

The product of a finite number of pseudoemetric spaces, with the max distance, is still a pseudoemetric space. This construction would also work for infinite products, but it would not give rise to the product topology. Hence, we only formalize it in the good situation of finitely many spaces.

Equations
source
instance emetricSpacePi {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EMetricSpace (π b)] :
EMetricSpace ((b : β) → π b)

The product of a finite number of emetric spaces, with the max distance, is still an emetric space. This construction would also work for infinite products, but it would not give rise to the product topology. Hence, we only formalize it in the good situation of finitely many spaces.

Equations