Theorems · Inductive type · functional analysis

IsBoundedBilinearMap

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

A map f : E × F → G satisfies IsBoundedBilinearMap 𝕜 f if it is bilinear and continuous.

Defined in

Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Cited by

40 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

SemiringSeminormedAddCommGroupModuleSeminormedAddCommGroupModuleSeminormedAddCommGroupModule