English
For every x0, the neighborhood filter in the topology generated by B equals the neighborhood function N_B(x0).
Русский
Для каждого x0 фильтр окрестностей в топологии, порождённой B, равен N_B(x0).
LaTeX
$$nhds\left( x_0 \right) = B.N x_0$$
Lean4
@[to_additive]
theorem nhds_eq (B : GroupFilterBasis G) {x₀ : G} : @nhds G B.topology x₀ = B.N x₀ :=
by
apply TopologicalSpace.nhds_mkOfNhds_of_hasBasis (fun x ↦ (FilterBasis.hasBasis _).map _)
· intro a U U_in
exact ⟨1, B.one U_in, mul_one a⟩
· intro a U U_in
rcases GroupFilterBasis.mul U_in with ⟨V, V_in, hVU⟩
filter_upwards [image_mem_map (B.mem_filter_of_mem V_in)]
rintro _ ⟨x, hx, rfl⟩
calc
(a * x) • V ∈ (a * x) • B.filter := smul_set_mem_smul_filter <| B.mem_filter_of_mem V_in
_ = a • x • V := smul_smul .. |>.symm
_ ⊆ a • (V * V) := (smul_set_mono <| smul_set_subset_smul hx)
_ ⊆ a • U := smul_set_mono hVU
