nhds_one_hasBasis — Mathlib

English

Let B be a GroupFilterBasis on G. Then the neighborhood basis at the identity element 1 is given by the sets in B, i.e., nhds(1) has basis { V : V ∈ B } with the same sets.

Русский

Пусть B — базис фильтра группы на группе G. Тогда базис окрестностей единицы 1 задаётся множествами из B: nhds(1) имеет базис { V | V ∈ B }.

LaTeX

$$$\operatorname{HasBasis}(\nhds 1)(\lambda V: V\in B)\,\mathrm{id}$.$$

Lean4

@[to_additive]
theorem nhds_one_hasBasis (B : GroupFilterBasis G) : HasBasis (@nhds G B.topology 1) (fun V : Set G ↦ V ∈ B) id :=
  by
  rw [B.nhds_one_eq]
  exact B.toFilterBasis.hasBasis

Похожие утверждения