withSeminorms — Mathlib

English

If a linear map f is inducing, and q has seminominal structure on F with associated topology, then the pullback seminorms q.comp f define a withSeminorms structure on E.

Русский

Если линейное отображение f индуктивно задаёт топологию на E и q имеет структуру семинорм на F, то отражённые назад семинорм q.comp f задают структуру withSeminorms на E.

LaTeX

$$$ IsInducing f \\Rightarrow q.withSeminorms_induced \\Rightarrow WithSeminorms (q.comp f) $$$

Lean4

theorem withSeminorms {q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q) [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F}
    (hf : IsInducing f) : WithSeminorms (q.comp f) :=
  by
  rw [hf.eq_induced]
  exact f.withSeminorms_induced hq

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