Skip to content
Journals Garden

Proposition II.2.2 (フィルター基底の内在的特徴づけ)

  • Proposition II.2.2 (フィルター基底の内在的特徴づけ) #Card
    • 空でない族 $\mathcal{B}$ が（何かの proper filter の）フィルター基底であるための条件。

Back

Section titled “Back”

A non-empty family $\mathcal{B}$ of subsets of $X$ is a filter-base if and only if $\emptyset \notin \mathcal{B}$ and for each $B_0, B_1 \in \mathcal{B}$, there exists $B \in \mathcal{B}$ such that $B \subset B_0 \cap B_1$.

（生成されるフィルターは $\mathcal{B}^\uparrow = {F : \exists B \in \mathcal{B},\ B \subset F}$。「下方に有向 ＋ 空を含まない」が基底の内在的な定義——第III章以降で新しいフィルターを作る際の標準チェック。）

証明の骨子:

  • （必要性）$\mathcal{B}$ が proper filter $\mathcal{F}$ の基底なら $\emptyset \notin \mathcal{B}$（$\mathcal{F}$ が proper）。また $B_0, B_1 \in \mathcal{B} \subset \mathcal{F}$ より $B_0 \cap B_1 \in \mathcal{F}$、基底の定義から $B \subset B_0 \cap B_1$ なる $B \in \mathcal{B}$ が取れる。
  • （十分性）条件を満たす $\mathcal{B}$ から $\mathcal{F} := \mathcal{B}^\uparrow$ を作ると、これがフィルターになる: isotone は $\uparrow$ の定義から自明。有限交叉閉性は、$F_0, F_1 \in \mathcal{F}$ に $B_0 \subset F_0$, $B_1 \subset F_1$ を取り、条件から $B \subset B_0 \cap B_1 \subset F_0 \cap F_1$ を得て $F_0 \cap F_1 \in \mathcal{F}$。proper 性は $\emptyset \notin \mathcal{B}$ から（$B \subset \emptyset$ なる $B$ は無い）。
  • 鍵は「有限交叉が基底の下に有向」を「二項の下界の存在」に落とすこと——空でない有限交叉が空でないことを保証する。

Lean

Section titled “Lean”

Filter.IsBasis（nonempty, inter_sets）；生成は FilterBasis.filter