Free Filter (自由フィルター) (Definition II.2.7)

• Free Filter (自由フィルター) (Definition II.2.7) #Card
  • A filter $\mathcal{F}$ is free if its kernel is empty: $\bigcap_{F \in \mathcal{F}} F = \emptyset$.

Back

A filter $\mathcal{F}$ is free if its kernel is empty: $\bigcap_{F \in \mathcal{F}} F = \emptyset$.

Lean

自由フィルター：Filter.ker f = ∅（本ノート II.4 の freePart 参照）