projectiveSeminorm_apply — Mathlib

English

Upgrading mapL to a MonoidHom when E = E′, giving a monoid hom from coordinatewise continuous linear maps to the corresponding tensor map.

Русский

Усовершенствование mapL до моноид-гомоморфа при E = E′, образующее моноид-гомоморф из координатно непрерывных линейных отображений к соответствующей карте на тензоре.

LaTeX

$$$ \\mathrm{mapLMonoidHom} : (\\Pi i, E_i \\toL[𝕜] E_i) \\to* ((⨂[𝕜] i, E_i) \\toL[𝕜] ⨂[𝕜] i, E_i) $$$

Lean4

theorem projectiveSeminorm_apply (x : ⨂[𝕜] i, E i) :
    projectiveSeminorm x = iInf (fun (p : lifts x) ↦ projectiveSeminormAux p.1) :=
  rfl

Похожие утверждения