Theorems · Inductive type · functional analysis

IsBoundedLinearMap

(𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : Semiring 𝕜] →
        [inst_1 : SeminormedAddCommGroup E] →
          [Module 𝕜 E] → [inst_3 : SeminormedAddCommGroup F] → [Module 𝕜 F] → (E → F) → Prop

A function f satisfies IsBoundedLinearMap 𝕜 f if it is linear and satisfies the inequality ‖f x‖ ≤ M * ‖x‖ for some positive constant M. (We put only the typeclasses strictly necessary for the definition, although the main case of interest is when 𝕜 itself is a normed ring and E, F are normed modules.)

Defined in

Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Cited by

39 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

SemiringSeminormedAddCommGroupModuleSeminormedAddCommGroupModule