Theorems · Inductive type · functional analysis

LinearIsometryEquiv

{R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        (σ₁₂ : R →+* R₂) →
          {σ₂₁ : R₂ →+* R} →
            [RingHomInvPair σ₁₂ σ₂₁] →
              [RingHomInvPair σ₂₁ σ₁₂] →
                (E : Type u_11) →
                  (E₂ : Type u_12) →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] → [Module R E] → [Module R₂ E₂] → Type (max u_11 u_12)

A semilinear isometric equivalence between two normed vector spaces, denoted as f : E ≃ₛₗᵢ[σ₁₂] E₂.

Defined in

Mathlib.Analysis.Normed.Operator.LinearIsometry

Cited by

748 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 92 definitions · uses no axioms

Assumes

SemiringSemiringRingHomInvPairRingHomInvPairSeminormedAddCommGroupSeminormedAddCommGroupModuleModule