continuousSMul_iInf — Mathlib

English

If ts' : ι → TopologicalSpace X and each provides a ContinuousSMul, then the infimum topology over i yields ContinuousSMul.

Русский

Если ts' : ι → TopologicalSpace X и для каждого i есть ContinuousSMul, то на пересечении (iInf) даёт ContinuousSMul.

LaTeX

$$ContinuousSMul M X on ⨅ i, ts'(i)$$

Lean4

@[to_additive]
theorem continuousSMul_iInf {ts' : ι → TopologicalSpace X} (h : ∀ i, @ContinuousSMul M X _ _ (ts' i)) :
    @ContinuousSMul M X _ _ (⨅ i, ts' i) :=
  continuousSMul_sInf <| Set.forall_mem_range.mpr h

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