weakBilin_withSeminorms — Mathlib

English

Another equivalent statement: membership in span is equivalent to a suitable continuity property in a finite-dimensional induced topology setting.

Русский

Еще одно эквивалентное утверждение: принадлежность span эквивалентна свойству непрерывности в заданной конечной размерности индуцированной топологии.

LaTeX

$$$\phi \in \mathrm{span}(\mathrm{range}(f)) \iff \text{Continuous}(\text{coefficient map of } \phi)$$$

Lean4

theorem weakBilin_withSeminorms (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    WithSeminorms (LinearMap.toSeminormFamily B : F → Seminorm 𝕜 (WeakBilin B)) :=
  let e : F ≃ (Σ _ : F, Fin 1) := .symm <| .sigmaUnique _ _
  withSeminorms_induced (withSeminorms_pi (fun _ ↦ norm_withSeminorms 𝕜 𝕜))
      (LinearMap.ltoFun 𝕜 F 𝕜 ∘ₗ B : (WeakBilin B) →ₗ[𝕜] (F → 𝕜)) |>.congr_equiv
    e

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