of_comm_of_nhds_one — Mathlib

English

If the multiplication is commutative (for all x,y) and the translation conditions hold, then G is a topological group.

Русский

Если умножение коммутативно и выполняются условия переноса, то G получается топологической группой.

LaTeX

$$$IsTopologicalGroup.of\_comm\_of\_nhds\_one(hmul)(hinv)(hleft)$$$

Lean4

@[to_additive]
theorem of_comm_of_nhds_one {G : Type u} [CommGroup G] [TopologicalSpace G]
    (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)) (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : G, 𝓝 x₀ = map (x₀ * ·) (𝓝 1)) : IsTopologicalGroup G :=
  IsTopologicalGroup.of_nhds_one hmul hinv hleft (by simpa using tendsto_id)

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