Lattice-Filter (束フィルター) (Remark III.7.7)

• Lattice-Filter (束フィルター) (Remark III.7.7) #Card
  • Let $(A, \leq)$ be a lattice. $F \subset A$ is a lattice-filter if $F \neq \emptyset$; $a \in F$ and $x \geq a$ imply $x \in F$; and $a_0, a_1 \in F$ imply $a_0 \wedge a_1 \in F$.

Back

Let $(A, \leq)$ be a lattice. Then $F \subset A$ is called a lattice-filter provided that:

1. $F \neq \emptyset$;
2. if $a \in F$ and $x \geq a$, then $x \in F$（上方閉）;
3. if $a_0, a_1 \in F$, then $a_0 \wedge a_1 \in F$（有限 meet で閉）.

• 集合フィルターは特別な場合: a filter $\mathcal{F}$ on $X$ is a lattice-filter on $(2^X, \subset)$（$A_0 \wedge A_1 = A_0 \cap A_1$）。
• cards/topology/prop-iii-7-8: 有限安定収束の $\xi^-(x)$ はフィルターの束上の lattice-filter。

Lean

Order.PFilter（順序集合上のフィルター、Order.Ideal の双対）。集合版が通常の Filter X