English
Two IsTopologicalGroup structures on G are equal if the nhds at 1 agree; an isomorphism of topologies via nhds is an equality.
Русский
Две структуры IsTopologicalGroup на G равны, если совпадают nhds в единице.
LaTeX
$$$IsTopologicalGroup\;ext\;\text{(конструкция)}$$$
Lean4
@[to_additive]
theorem of_nhds_one {G : Type*} [Group G] [TopologicalSpace G] (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
(hleft : ∀ x₀ : G, 𝓝 x₀ = map (fun x : G => x₀ * x) (𝓝 1))
(hconj : ∀ x₀ : G, Tendsto (fun x : G => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)) : ContinuousInv G :=
by
refine ⟨continuous_iff_continuousAt.2 fun x₀ => ?_⟩
have : Tendsto (fun x => x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (x₀⁻¹ * ·) (𝓝 1)) :=
(tendsto_map.comp <| hconj x₀).comp hinv
simpa only [ContinuousAt, hleft x₀, hleft x₀⁻¹, tendsto_map'_iff, Function.comp_def, mul_assoc, mul_inv_rev,
inv_mul_cancel_left] using this
