hasBasis — Mathlib

English

For each x, B.N x has a basis given by the sets V ∈ B, with the base sets being the image of V under the map y ↦ x y.

Русский

Для каждого x база B.N x имеет базис, состоящий из образов множества V ∈ B под отображением y ↦ x y.

LaTeX

$$HasBasis (B.N x) (fun V => V ∈ B) (fun V => (fun y => x * y) '' V)$$

Lean4

@[to_additive]
protected theorem hasBasis (B : GroupFilterBasis G) (x : G) :
    HasBasis (B.N x) (fun V : Set G ↦ V ∈ B) fun V ↦ (fun y ↦ x * y) '' V :=
  HasBasis.map (fun y ↦ x * y) toFilterBasis.hasBasis

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