English
A constructive IsTopologicalGroup structure can be built from hmul, hinv, hleft, hconj with a limit at (1,1).
Русский
Из заданных условий можно построить структуру IsTopologicalGroup на G.
LaTeX
$$$IsTopologicalGroup.of\_nhds\_one(hmul)(hinv)(hleft)(hconj)$$$
Lean4
@[to_additive]
theorem of_nhds_one {G : Type u} [Group 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)) (hconj : ∀ x₀ : G, Tendsto (x₀ * · * x₀⁻¹) (𝓝 1) (𝓝 1)) :
IsTopologicalGroup G :=
by
refine IsTopologicalGroup.of_nhds_one' hmul hinv hleft fun x₀ => ?_
replace hconj : ∀ x₀ : G, map (x₀ * · * x₀⁻¹) (𝓝 1) = 𝓝 1 := fun x₀ =>
map_eq_of_inverse (x₀⁻¹ * · * x₀⁻¹⁻¹) (by ext; simp [mul_assoc]) (hconj _) (hconj _)
rw [← hconj x₀]
simpa [Function.comp_def] using hleft _
