injectiveSeminorm_apply — Mathlib

English

The injective seminorm on the tensor equals the supremum over a bounded family of seminorms evaluated at x.

Русский

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

LaTeX

$$injectiveSeminorm x = sup_p p(x)$$

Lean4

theorem injectiveSeminorm_apply (x : ⨂[𝕜] i, E i) :
    injectiveSeminorm x =
      ⨆ p :
        {p |
          ∃ (G : Type (max uι u𝕜 uE)) (_ : SeminormedAddCommGroup G) (_ : NormedSpace 𝕜 G),
            p =
              Seminorm.comp (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
                (toDualContinuousMultilinearMap G (𝕜 := 𝕜) (E := E))},
        p.1 x :=
  by simpa only [injectiveSeminorm, Set.coe_setOf, Set.mem_setOf_eq] using Seminorm.sSup_apply dualSeminorms_bounded

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