dualSeminorms_bounded — Mathlib

English

The collection of dual-induced seminorms is bounded above by a projective seminorm; hence their supremum is finite on the tensor product.

Русский

Коллекция двойственно-индукцированных полунорм ограничена сверху проектной полунормой; её супремум конечен на тензорном произведении.

LaTeX

$$BddAbove { p | ∃ G, seminorm on G, p = Seminorm.comp (...) }$$

Lean4

theorem dualSeminorms_bounded :
    BddAbove
      {p |
        ∃ (G : Type (max uι u𝕜 uE)) (_ : SeminormedAddCommGroup G) (_ : NormedSpace 𝕜 G),
          p =
            Seminorm.comp (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
              (toDualContinuousMultilinearMap G (𝕜 := 𝕜) (E := E))} :=
  by
  existsi projectiveSeminorm
  rw [mem_upperBounds]
  simp only [Set.mem_setOf_eq, forall_exists_index]
  intro p G _ _ hp
  rw [hp]
  intro x
  simp only [Seminorm.comp_apply, coe_normSeminorm]
  exact toDualContinuousMultilinearMap_le_projectiveSeminorm _

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