N — Mathlib · SciLib

English

The neighborhood function of a GroupFilterBasis is given by N(B)(x) = map (y ↦ x y) of the filter B.

Русский

Функция окрестностей группы-основы задаётся как N(B)(x) = образ отображения y ↦ x y применительно к фильтру B.

LaTeX

$$N(B)(x) := map (fun y => x * y) B.toFilterBasis.filter$$

Lean4

/-- The neighborhood function of a `GroupFilterBasis`. -/
@[to_additive /-- The neighborhood function of an `AddGroupFilterBasis`. -/
    ]
def N (B : GroupFilterBasis G) : G → Filter G := fun x ↦ map (fun y ↦ x * y) B.toFilterBasis.filter

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