Polyhedral Filter / Product Filter (多面体フィルター / 積フィルター) (Definition IV.6.4)
- Polyhedral Filter / Product Filter (多面体フィルター / 積フィルター) (Definition IV.6.4) #Card
- A polyhedron in $\prod_{j \in J} X_j$ is a set $D = \prod_j D_j$ with ${j : D_j \neq X_j}$ finite. A filter is polyhedral if it has a filter-base of polyhedra — equivalently, iff it is a product filter (Proposition IV.6.5).
A subset of $\prod_{j \in J} X_j$ is a polyhedron if it is of the form $D = \prod_{j \in J} D_j$ where ${j \in J : D_j \neq X_j}$ is finite——equivalently $D = \bigcap_{j \in J_0} p_j^-(D_j)$ for finite $J_0$（有限個の座標だけ制限した「筒集合」）. A filter on $\prod_j X_j$ is polyhedral if it has a filter-base made of polyhedra.
- Product filter: $\prod_{j \in J} \mathcal{F}j := \bigvee{j \in J} p_j^-[\mathcal{F}_j]$。
- Proposition IV.6.5: a filter is polyhedral $\iff$ it is a product filter。
- 測度論の cylinder sets（筒集合族）の原型。積収束で $\varphi$ に収束する最粗フィルターは polyhedral。
Filter.pi（Filter.mem_pi：有限個の座標で決まる基底）