topologicalGroup_iInf — Mathlib

English

If a family of topologies ts' on G makes G a topological group for every index, then the indexed infimum of those topologies yields a topological group structure on G.

Русский

Если множество топологий ts' на G делает G топологической группой для каждого индекса, то инфимума этих топологий задаёт топологическую группу на G.

LaTeX

$$$ \\forall i, IsTopologicalGroup(G, ts'(i)) \\Rightarrow IsTopologicalGroup(G, \\inf_i ts'(i)) $$$

Lean4

@[to_additive]
theorem topologicalGroup_iInf {ts' : ι → TopologicalSpace G} (h' : ∀ i, @IsTopologicalGroup G (ts' i) _) :
    @IsTopologicalGroup G (⨅ i, ts' i) _ := by
  rw [← sInf_range]
  exact topologicalGroup_sInf (Set.forall_mem_range.mpr h')

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