手筋: mod-finite（有限を無視する）論法 (Ex II.5.7)
- 手筋: mod-finite（有限を無視する）論法 (Ex II.5.7) #Card
- cofinite filter・almost equality まわりで「有限集合の差を無視して」議論する手筋は？
核: cofinite filter は台集合の有限修正で不変: $$(B)_0 = (D)_0 \iff B \triangle D \text{ が有限} \qquad \text{(Ex II.5.7)}$$ 片側版は $(B)_0 \subset (D)_0 \iff D \setminus B$ 有限。
運用.
- 包含を示すときは $D \subset B \cup (D \setminus B)$ 型の分解で「有限のゴミ」$B_F, D_B$ を右辺に押し付け、有限和が有限であることで吸収する。
- 破るときは無限差 $D \setminus B$ から証人（$B \in (B)_0 \setminus (D)_0$）を出す。
- cards/topology/almost-equal（$B \triangle D$ 有限）は同値関係で、subcofinite filter（cards/topology/subcofinite-almost-principal-filter）は「almost equal な基を持つフィルター」と特徴づけられる（Prop II.5.10）。
射程: 「小さい集合のイデアルを法として同一視する」議論の最小例（イデアル＝有限集合）。測度論では有限集合 → 零集合、almost equal → a.e. 等しい、$(B)_0$ の不変性 → $L^p$ 元が同値類であることに対応する。イデアルを可算集合に替えれば cocountable filter（Ex II.5.5）の議論になる。
Mathlib では Filter.cofinite と Set.Finite.symmDiff 系。「mod-finite で filter 不変」は Filter.cofinite の EventuallyEq（=ᶠ[cofinite]）として表現される。