iInf — Mathlib

English

If ts' is an indexed family of locally convex spaces on E, then the infimum of their topologies is again a locally convex space on E.

Русский

Если имеется индексированная семейство локально выпуклых пространств на E, то инфимума их топологий снова образует локально выпуклое пространство на E.

LaTeX

$$$\forall i,\; \text{LocallyConvexSpace } 𝕜 E \Rightarrow \text{LocallyConvexSpace } 𝕜 E \, (\bigwedge_i \tau_i)$$$

Lean4

protected theorem iInf {ts' : ι → TopologicalSpace E} (h' : ∀ i, @LocallyConvexSpace 𝕜 E _ _ _ _ (ts' i)) :
    @LocallyConvexSpace 𝕜 E _ _ _ _ (⨅ i, ts' i) :=
  .sInf <| by rwa [forall_mem_range]

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