Theorems · Definition · functional analysis

lp.singleContinuousAddMonoidHom

{α : Type u_3} →
  (E : α → Type u_4) →
    (p : ENNReal) →
      [inst : (i : α) → NormedAddCommGroup (E i)] →
        [DecidableEq α] → [inst_2 : Fact (1 ≤ p)] → (i : α) → E i →ₜ+ ↥(lp E p)

lp.single as a continuous morphism of additive monoids.

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupDecidableEqFact