Theorems · Definition · functional analysis

SeminormFamily.basisSets

{R : Type u_1} →
  {E : Type u_6} →
    {ι : Type u_9} →
      [inst : SeminormedRing R] → [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → SeminormFamily R E ι → Set (Set E)

The sets of a filter basis for the neighborhood filter of 0.

Defined in

Mathlib.Analysis.LocallyConvex.WithSeminorms

Cited by

22 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedRingAddCommGroupModule