English
If ts is a set of topological spaces on E and every ts-element makes E into a locally convex space, then the infimum topology sInf ts also makes E locally convex.
Русский
Если ts — множество топологических структур на E, и каждая из них делает E локально выпуклым пространством, то инфимум топологий sInf ts также делает E локально выпуклым.
LaTeX
$$$\Big(\forall t \in ts,\ \text{LocallyConvexSpace } 𝕜 E\Big) \Rightarrow \text{LocallyConvexSpace } 𝕜 E \, (sInf ts).$$$
Lean4
protected theorem sInf {ts : Set (TopologicalSpace E)} (h : ∀ t ∈ ts, @LocallyConvexSpace 𝕜 E _ _ _ _ t) :
@LocallyConvexSpace 𝕜 E _ _ _ _ (sInf ts) :=
by
letI : TopologicalSpace E := sInf ts
refine
.ofBases 𝕜 E (fun _ => fun If : Set ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
(fun x => fun If : Set ts × (ts → Set E) => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ @nhds _ (↑i) x ∧ Convex 𝕜 (If.2 i))
(fun x => ?_) fun x If hif => convex_iInter fun i => convex_iInter fun hi => (hif.2 i hi).2
rw [nhds_sInf, ← iInf_subtype'']
exact .iInf' fun i : ts => (@locallyConvexSpace_iff 𝕜 E _ _ _ _ ↑i).mp (h (↑i) i.2) x
