Theorems · Theorem · functional analysis

PiLp.single_apply

∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : Zero 𝕜] (i : ι) (a : 𝕜) (j : ι),
  (PiLp.single p i a).ofLp j = if j = i then a else 0

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

11 results in Mathlib

Foundations

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

Assumes

DecidableEqZero