English
The neighborhood basis at the identity in the quotient is generated by balls around 1, giving a basis { x : ∥x∥ < ε } as ε → 0.
Русский
Базис окрестностей единицы в факторгруппе задаётся шаровыми окрестностями вокруг 1, формируя набор {x : ∥x∥ < ε} при ε → 0.
LaTeX
$$$\mathcal{N}(1) = \{ B(1, \varepsilon) : \varepsilon > 0 \}$ and has basis { x : ∥x∥ < ε }.$$
Lean4
@[to_additive]
theorem nhds_one_hasBasis : (𝓝 (1 : M ⧸ S)).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε} :=
by
have : ∀ ε : ℝ, mk '' ball (1 : M) ε = {x : M ⧸ S | ‖x‖ < ε} :=
by
refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
rw [ball_one_eq, mem_setOf_eq, norm_lt_iff, mem_image]
exact exists_congr fun _ ↦ and_comm
rw [← mk_one, nhds_eq, ← funext this]
exact .map _ Metric.nhds_basis_ball
