Theorems · Definition · functional analysis

PiLp

ENNReal → {ι : Type u_1} → (ι → Type u_2) → Type (max u_1 u_2)

A copy of a Pi type, on which we will put the L^p distance. Since the Pi type itself is already endowed with the L^∞ distance, we need the type synonym to avoid confusing typeclass resolution. Also, we let it depend on p, to get a whole family of type on which we can put different distances.

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

150 results in Mathlib

Foundations

Depth 98 from the axioms, rests on 1,957 definitions · uses propext, Classical.choice, Quot.sound