continuous_iff_continuous_comp — Mathlib

English

In a normed space context, if a family of seminorms bounds a linear map, then the map is continuous.

Русский

В контексте нормированного пространства, если семейство семинорм ограничивает линейное отображение, то отображение непрерывно.

LaTeX

$$$cont_withSeminorms_normedSpace:\\; (hp : WithSeminorms p) \\Rightarrow (f: E→_{τ_1} F) \\rightarrow \\text{ Continuous } f$$$

Lean4

theorem continuous_iff_continuous_comp {q : SeminormFamily 𝕝₂ F ι'} [TopologicalSpace E] [IsTopologicalAddGroup E]
    [TopologicalSpace F] (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) : Continuous f ↔ ∀ i, Continuous ((q i).comp f) :=
  ⟨fun h i => (hq.continuous_seminorm i).comp h, continuous_of_continuous_comp hq f⟩

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