continuous_seminorm — Mathlib

English

Every seminorm p_i in a separating family p is a continuous seminorm with respect to the induced topology.

Русский

Каждая семинормa p_i из семейства p непрерывна относительно индукции топологии.

LaTeX

$$$hp:\\; WithSeminorms\\ p \\Rightarrow\\forall i,\\text{Continuous }(p_i)$$$

Lean4

theorem continuous_seminorm {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) (i : ι) : Continuous (p i) :=
  by
  have := hp.topologicalAddGroup
  rw [p.withSeminorms_iff_topologicalSpace_eq_iInf.mp hp]
  exact continuous_iInf_dom (@continuous_norm _ (p i).toSeminormedAddGroup)

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