projectiveSeminorm_tprod_le — Mathlib

English

For a family (m_i) of elements, projectiveSeminorm on the tensor tprod ≤ ∏ ∥m_i∥.

Русский

Для семейства элементов m_i: projectiveSeminorm на тензоре tprod ≤ ∏ ∥m_i∥.

LaTeX

$$$ \\mathrm{projectiveSeminorm}(\\mathrm{tprod}_{i} m_i) \\leq \\prod_i \\|m_i\\| $$$

Lean4

theorem projectiveSeminorm_tprod_le (m : Π i, E i) : projectiveSeminorm (⨂ₜ[𝕜] i, m i) ≤ ∏ i, ‖m i‖ :=
  by
  rw [projectiveSeminorm_apply]
  convert ciInf_le (bddBelow_projectiveSemiNormAux _) ⟨FreeAddMonoid.of ((1 : 𝕜), m), ?_⟩
  · simp [projectiveSeminormAux]
  · rw [mem_lifts_iff, FreeAddMonoid.toList_of, List.map_singleton, List.sum_singleton, one_smul]

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