continuousMul_iInf — Mathlib

English

Given a family ts of topologies on M, if each topology ts i makes multiplication continuous, then the infimum over i, sInf ts, also makes multiplication continuous.

Русский

Если у нас есть семейство топологий ts на M и каждая из них делает умножение непрерывным, то инфимуум по i, sInf ts, тоже делает умножение непрерывным.

LaTeX

$$$\\forall i,\\ ContinuousMul M \\text{ under } ts i \\Rightarrow ContinuousMul M$$

Lean4

@[to_additive]
theorem continuousMul_iInf {ts : ι' → TopologicalSpace M} (h' : ∀ i, @ContinuousMul M (ts i) _) :
    @ContinuousMul M (⨅ i, ts i) _ := by
  rw [← sInf_range]
  exact continuousMul_sInf (Set.forall_mem_range.mpr h')

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