addGroupFilterBasis — Mathlib

English

The addGroupFilterBasis on E is the filter basis generated from p.basisSets and the accompanying lemmas about their interactions with addition, zero, and negation.

Русский

Фильтр-база для аддитивной группы на E строится из p.basisSets и сопутствующих лемм об их взаимодействии с сложением, нулём и отрицанием.

LaTeX

$${AddGroupFilterBasis E}$$

Lean4

/-- The `addGroupFilterBasis` induced by the filter basis `Seminorm.basisSets`. -/
protected def addGroupFilterBasis : AddGroupFilterBasis E :=
  addGroupFilterBasisOfComm p.basisSets p.basisSets_nonempty p.basisSets_intersect p.basisSets_zero p.basisSets_add
    p.basisSets_neg

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