English
If ts is a set of topologies on M and each makes multiplication continuous, then the infimum topology sInf ts also makes multiplication continuous.
Русский
Если множество топологий ts на M таково, что каждая из них делает умножение непрерывным, то инфимуум топологий sInf ts тоже делает умножение непрерывным.
LaTeX
$$$\\forall t \\in ts,\\ ContinuousMul\\ M \\text{ under } t\\;\\Rightarrow\\; ContinuousMul M\\text{ under } \\mathrm{sInf}\\ ts$$
Lean4
@[to_additive]
theorem continuousMul_sInf {ts : Set (TopologicalSpace M)} (h : ∀ t ∈ ts, @ContinuousMul M t _) :
@ContinuousMul M (sInf ts) _ :=
letI := sInf ts
{
continuous_mul :=
continuous_sInf_rng.2 fun t ht => continuous_sInf_dom₂ ht ht (@ContinuousMul.continuous_mul M t _ (h t ht)) }
