English
For a family ts' of topological spaces, if each is locally convex, the infimum over i of ts' i is locally convex.
Русский
Для семейства топологий ts' каждая из которых локально выпукла, инфимум по i топологий ts' i остаётся локально выпуклым.
LaTeX
$$$\forall i,\; \text{LocallyConvexSpace } 𝕜 E \Rightarrow \text{LocallyConvexSpace } 𝕜 E \ (⨅ i, ts' i)$$$
Lean4
/-- Scalar multiplication `• : R × A → A` is continuous if `R` is a topological
ring, and `A` is an `R` module with the module topology. -/
theorem continuousSMul : @ContinuousSMul R A _ _ (moduleTopology R A) :=
/- Proof: We need to prove that the product topology is finer than the pullback
of the module topology. But the module topology is an Inf and thus a limit,
and pullback is a right adjoint, so it preserves limits.
We must thus show that the product topology is finer than an Inf, so it suffices
to show it's a lower bound, which is not hard. All this is wrapped into
`continuousSMul_sInf`.
-/
continuousSMul_sInf fun _ h ↦ h.1
