English
If p is a family of seminorms generating a topology, then i ↦ Finset.Iic i .sup p also generates the same topology under the same assumptions with locally finite order.
Русский
Если p — семейство семинорм, порождающее топологию, то i ↦ Finset.Iic i .sup p также порождает ту же топологию при тех же предположениях об локально конечном порядке.
LaTeX
$$$ WithSeminorms p \\to WithSeminorms (\\lambda i, (Finset.Iic i).sup p) $$$
Lean4
protected theorem partial_sups [Preorder ι] [LocallyFiniteOrderBot ι] {p : SeminormFamily 𝕜 E ι} [TopologicalSpace E]
(hp : WithSeminorms p) : WithSeminorms (fun i ↦ (Finset.Iic i).sup p) :=
by
refine hp.congr ?_ ?_
· intro i
refine ⟨Finset.Iic i, 1, ?_⟩
rw [one_smul]
rfl
· intro i
refine ⟨{ i }, 1, ?_⟩
rw [Finset.sup_singleton, one_smul]
exact (Finset.le_sup (Finset.mem_Iic.mpr le_rfl) : p i ≤ (Finset.Iic i).sup p)
