finset_sups — Mathlib

English

If p is a family of seminorms generating a topology, then the family s ↦ s.sup p, indexed by finite sets s, also generates the same topology when used as a seminorm family.

Русский

Если p — семейство семинорм, порождающее топологию, то семейство s ↦ s.sup p, индексируемое конечными множествами s, также порождает ту же топологию.

LaTeX

$$$ WithSeminorms p \\to WithSeminorms (\\lambda s: Finset ι, s.sup p) $$$

Lean4

protected theorem finset_sups {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E] (hp : WithSeminorms p) :
    WithSeminorms (fun s : Finset ι ↦ s.sup p) :=
  by
  refine hp.congr ?_ ?_
  · intro s
    refine ⟨s, 1, ?_⟩
    rw [one_smul]
    rfl
  · intro i
    refine ⟨{{ i }}, 1, ?_⟩
    rw [Finset.sup_singleton, Finset.sup_singleton, one_smul]
    rfl

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