isUniformGroup_iInf — Mathlib

English

If each us'(i) endows G with a uniform group structure, then the infimum over i of us'(i) also yields a uniform group structure on G.

Русский

Если для каждого i глаз uniform space us'(i) делает G равномерной группой, то инфимум по i также задает равномерную группу.

LaTeX

$$$\forall i, IsUniformGroup G \Rightarrow IsUniformGroup G (iInf us').$$$

Lean4

@[to_additive]
theorem isUniformGroup_iInf {ι : Sort*} {us' : ι → UniformSpace G} (h' : ∀ i, @IsUniformGroup G (us' i) _) :
    @IsUniformGroup G (⨅ i, us' i) _ := by
  rw [← sInf_range]
  exact isUniformGroup_sInf (Set.forall_mem_range.mpr h')

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