English
If a linear map is bounded with respect to a family of seminorms against a constant seminorm q, then it is bounded with respect to a finite sup of p, and conversely.
Русский
Если линейное отображение ограничено относительно семейства полунорм против константы q, то ограниченно и относительно конечной суммы sup p; обратно — аналогично.
LaTeX
$$IsBounded p (fun _ : ι' => q) f ↔ ∀ i, ∃ C, (q i).comp f ≤ C • p$$
Lean4
/-- If a family of seminorms is continuous, then their basis sets are neighborhoods of zero. -/
theorem basisSets_mem_nhds {𝕜 E ι : Type*} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
(p : SeminormFamily 𝕜 E ι) (hp : ∀ i, Continuous (p i)) (U : Set E) (hU : U ∈ p.basisSets) : U ∈ 𝓝 (0 : E) :=
by
obtain ⟨s, r, hr, rfl⟩ := p.basisSets_iff.mp hU
clear hU
refine Seminorm.ball_mem_nhds ?_ hr
classical
induction s using Finset.induction_on with
| empty => simpa using continuous_zero
| insert a s _ hs =>
simp only [Finset.sup_insert, coe_sup]
exact Continuous.max (hp a) hs
