English
If a family ts of topologies on X each supports a continuous SMul by M, then the infimum topology sInf ts also supports a continuous SMul.
Русский
Если множество топологий ts на X каждый поддерживает непрерывное действие M, то их пересечение (нижняя граница) тоже поддерживает непрерывное SMul.
LaTeX
$$ContinuousSMul M X on sInf ts$$
Lean4
@[to_additive]
theorem continuousSMul_sInf {ts : Set (TopologicalSpace X)} (h : ∀ t ∈ ts, @ContinuousSMul M X _ _ t) :
@ContinuousSMul M X _ _ (sInf ts) :=
let _ := sInf ts
{
continuous_smul := by
-- Porting note: needs `( :)`
rw [← (sInf_singleton (a := ‹TopologicalSpace M›) :)]
exact
continuous_sInf_rng.2 fun t ht =>
continuous_sInf_dom₂ (Eq.refl _) ht (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht)) }
