Indexed product of extended metric spaces

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) }

theorem edist_pi_def {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] (f : (b : β) → π b) (g : (b : β) → π b) : edist f g = Finset.univ.sup fun (b : β) => edist (f b) (g b)

theorem edist_le_pi_edist {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] (f : (b : β) → π b) (g : (b : β) → π b) (b : β) : edist (f b) (g b) ≤ edist f g

theorem edist_pi_le_iff {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {d : ENNReal} : edist f g ≤ d ↔ ∀ (b : β), edist (f b) (g b) ≤ d

theorem edist_pi_const_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Fintype β] (a : α) (b : α) : (edist (fun (x : β) => a) fun (x : β) => b) ≤ edist a b

@[simp]

theorem edist_pi_const {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Fintype β] [Nonempty β] (a : α) (b : α) : (edist (fun (x : β) => a) fun (x : β) => b) = edist a b

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

• pseudoEMetricSpacePi = PseudoEMetricSpace.mk ⋯ ⋯ ⋯ (Pi.uniformSpace π) ⋯

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

• emetricSpacePi = EMetricSpace.ofT0PseudoEMetricSpace ((b : β) → π b)