Filter

集合 $X$ の部分集合族 $\mathcal{F}$ のうち、isotone（上位集合で閉じる）かつ finitely complete（有限交叉で閉じる）なものを filter と呼ぶ。「十分小さい・十分先の集合の集まり」を公理化したもので、点列の「ある番号から先」や点の「近傍」を統一的に扱うための基礎道具。数学全般で「eventually / almost every」に類する概念（測度論の測度0の補集合、関数解析の弱位相の近傍系など）は多くがフィルターの言葉に翻訳できる。

書籍別カード

• Royal Road to Topology: cards/topology/filter — isotone + finitely complete な部分集合族として導入（proper 性は非退化性として別扱い）。関連カード: cards/topology/proper-filter（$\emptyset\notin\mathcal{F}$）、cards/topology/ultrafilter、cards/topology/principal-filter。

用語対応（terminology-map）

30_Concepts/topology-terminology-map（PR #168、本ノート作成時点で未マージ）「フィルター・収束の基礎語彙」節に該当行あり:

filter（cards/topology/filter） | filter | Filter

Royal Road の filter は improper（$\emptyset \in \mathcal{F}$）を許さない流儀だが、Mathlib の Filter は improper も許容し、非退化性は Filter.NeBot インスタンスで別途表現する。