injectiveSeminorm_tprod_le — Mathlib

English

The injective seminorm on the tensor product is dominated by the projective seminorm; hence, it is bounded by the product of seminorms on factors.

Русский

Инъективная полунормированность на тензорном произведении доминируется проективной нормой; следовательно, она ограничена произведением норм на факторе.

LaTeX

$$injectiveSeminorm ≤ projectiveSeminorm$$

Lean4

theorem injectiveSeminorm_tprod_le (m : Π (i : ι), E i) : injectiveSeminorm (⨂ₜ[𝕜] i, m i) ≤ ∏ i, ‖m i‖ :=
  le_trans (injectiveSeminorm_le_projectiveSeminorm _) (projectiveSeminorm_tprod_le m)

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