isUniformGroup_inf — Mathlib

English

The infimum of two uniform structures u1 and u2 on G, each making G a uniform group, also makes G a uniform group.

Русский

Пересечение (мера инфимума) двух униформных структур, делающих G равномерной группой, тоже образует равномерную группу.

LaTeX

$$$\text{IsUniformGroup } G (u_1) \land \text{IsUniformGroup } G (u_2) \Rightarrow \text{IsUniformGroup } G (u_1 \inf u_2).$$$

Lean4

@[to_additive]
theorem isUniformGroup_inf {u₁ u₂ : UniformSpace G} (h₁ : @IsUniformGroup G u₁ _) (h₂ : @IsUniformGroup G u₂ _) :
    @IsUniformGroup G (u₁ ⊓ u₂) _ := by
  rw [inf_eq_iInf]
  refine isUniformGroup_iInf fun b => ?_
  cases b <;> assumption

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