English
Let G be a group equipped with a group filter basis B. Then for every x0 in G the neighborhood system at x0 has a basis consisting of the left translates x0 · V with V in B; i.e. the basis around x0 is { x0 · V : V ∈ B }.
Русский
Пусть G — группа, снабжённая базисом фильтра B для группы. Тогда в любой точке x0 ∈ G окрестности образуют базис из левых переносов x0 · V, где V ∈ B; то есть базис окрестностей точки x0 состоит из множеств x0 · V, с V ∈ B.
LaTeX
$$$\operatorname{HasBasis}(\nhds x_0)\big(\lambda V: V\in B\big)\big(\lambda V, x_0 \cdot V\big)$.$$
Lean4
@[to_additive]
theorem nhds_hasBasis (B : GroupFilterBasis G) (x₀ : G) :
HasBasis (@nhds G B.topology x₀) (fun V : Set G ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V :=
by
rw [B.nhds_eq]
apply B.hasBasis
