isUniformGroup_sInf — Mathlib

English

If a group G is endowed with a family us of uniform spaces such that each makes G a uniform group, then the infimum sInf us also makes G a uniform group.

Русский

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

LaTeX

$$$\forall u \in us, IsUniformGroup\ G\;\Rightarrow\; IsUniformGroup\ G (sInf us).$$$

Lean4

@[to_additive]
theorem isUniformGroup_sInf {us : Set (UniformSpace G)} (h : ∀ u ∈ us, @IsUniformGroup G u _) :
    @IsUniformGroup G (sInf us) _ :=
  @IsUniformGroup.mk G (_) _ <|
    uniformContinuous_sInf_rng.mpr fun u hu =>
      uniformContinuous_sInf_dom₂ hu hu (@IsUniformGroup.uniformContinuous_div G u _ (h u hu))

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