English
If a neighborhood basis at 1 is given, then nhds at any x has a translated basis given by y with y/x ∈ s_i.
Русский
Если для единицы задана база окрестностей, то nhds в любой точке x имеет перенесённую базу через отношение y/x ∈ s_i.
LaTeX
$$$\text{HasBasis} (\mathcal{N}_{1}) p s \Rightarrow \mathcal{N}_{x} p (\lambda i. \{ y : y/x \in s(i) \})$$$
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 (fun x => x₀ * x) (𝓝 1)) (hright : ∀ x₀ : G, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) :
IsTopologicalGroup G :=
{ toContinuousMul := ContinuousMul.of_nhds_one hmul hleft hright
toContinuousInv :=
ContinuousInv.of_nhds_one hinv hleft fun x₀ =>
le_of_eq
(by
rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ← map_map, ← hleft,
hright, map_map]
simp) }
