Theorems · Definition · functional analysis

LinearIsometry.inl

(𝕜 : Type u_9) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_10) →
      (F : Type u_11) →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] → [inst_3 : SeminormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → E →ₗᵢ[𝕜] E × F

The injection x ↦ LinearMap.inl E F x as a linear isometry.

Defined in

Mathlib.Analysis.Normed.Operator.NormedSpace

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpace