topologicalGroup_inf — Mathlib

English

If G is a group and t1,t2 are topologies on G making G a topological group, then their infimum t1 ⊓ t2 also makes G a topological group.

Русский

Если G — группа и t1,t2 — топологии на G, делающие G топологической группой, то их пересечение t1 ⊓ t2 тоже образует топологическую группу.

LaTeX

$$$ IsTopologicalGroup G (t_1 \\sqcap t_2) $$$

Lean4

@[to_additive]
theorem topologicalGroup_inf {t₁ t₂ : TopologicalSpace G} (h₁ : @IsTopologicalGroup G t₁ _)
    (h₂ : @IsTopologicalGroup G t₂ _) : @IsTopologicalGroup G (t₁ ⊓ t₂) _ :=
  by
  rw [inf_eq_iInf]
  refine topologicalGroup_iInf fun b => ?_
  cases b <;> assumption

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