Theorems · Definition · functional analysis

SemilinearIsometryClass.recOn

{𝓕 : Type u_11} →
  {R : Type u_12} →
    {R₂ : Type u_13} →
      [inst : Semiring R] →
        [inst_1 : Semiring R₂] →
          {σ₁₂ : R →+* R₂} →
            {E : Type u_14} →
              {E₂ : Type u_15} →
                [inst_2 : SeminormedAddCommGroup E] →
                  [inst_3 : SeminormedAddCommGroup E₂] →
                    [inst_4 : Module R E] →
                      [inst_5 : Module R₂ E₂] →
                        [inst_6 : FunLike 𝓕 E E₂] →
                          {motive : SemilinearIsometryClass 𝓕 σ₁₂ E E₂ → Sort u} →
                            (t : SemilinearIsometryClass 𝓕 σ₁₂ E E₂) →
                              ([toSemilinearMapClass : SemilinearMapClass 𝓕 σ₁₂ E E₂] →
                                  (norm_map : ∀ (f : 𝓕) (x : E), ‖f x‖ = ‖x‖) → motive ⋯) →
                                motive t

Defined in

Mathlib.Analysis.Normed.Operator.LinearIsometry

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

SemiringSemiringSeminormedAddCommGroupSeminormedAddCommGroupModuleModuleFunLike