Theorems · Definition · functional analysis

LinearIsometry.single

{ι : Type u_9} →
  [inst : Fintype ι] →
    [DecidableEq ι] →
      (𝕜 : Type u_10) →
        [inst_2 : NontriviallyNormedField 𝕜] →
          (E : ι → Type u_11) →
            [inst_3 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] → (i : ι) → E i →ₗᵢ[𝕜] (j : ι) → E j

The injection x ↦ Pi.single i x as a linear isometry.

Defined in

Mathlib.Analysis.Normed.Operator.NormedSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqNontriviallyNormedFieldSeminormedAddCommGroupNormedSpace