Theorems · Definition · functional analysis

PiLp.pseudoMetricSpaceToPi

(p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) →
      [Fact (1 ≤ p)] → [Fintype ι] → [(i : ι) → PseudoMetricSpace (α i)] → PseudoMetricSpace ((i : ι) → α i)

This definition allows to endow Π i, α i with the Lp distance with the uniformity and bornology being defeq to the product ones. It is useful to endow a type synonym of Π i, α i with the Lp distance.

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

2 results in Mathlib

Foundations

Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactFintypePseudoMetricSpace