schwartz_withSeminorms — Mathlib

English

SchwartzMap carries a locally convex space structure compatible with its seminorm family.

Русский

SchwartzMap имеет локально выпуклую структуру, согласованную с семейством семинорм.

LaTeX

$$$\text{instLocallyConvexSpace} : \text{LocallyConvexSpace}$ on $\mathcal{S}(E,F)$$$

Lean4

theorem _root_.schwartz_withSeminorms : WithSeminorms (schwartzSeminormFamily 𝕜 E F) :=
  by
  have A : WithSeminorms (schwartzSeminormFamily ℝ E F) := ⟨rfl⟩
  rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf] at A ⊢
  rw [A]
  rfl

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