Net（ネット）と収束（Definition VII.6.2）
- Net（ネット）と収束（Definition VII.6.2） #Card
- directed set・net の定義と、ネットの収束をフィルターに帰着する仕組みは。
Directed set $(V,\leq)$: 前順序で $\forall v_0,v_1 \exists v,\ v_0\leq v \wedge v_1 \leq v$。$V^\uparrow(v) := {w : v\leq w}$（後続集合）の族 $\mathbb{V} := {V^\uparrow(v)}$ はフィルター基（Prop VII.6.1）— これを $\mathbb{V}^\uparrow$ と書く。
Net: $\varphi \in X^V$（$(V,\leq)$ は有向集合）。位相 $\tau$ で $\varphi$ が $x$ に収束 :⟺ 各 $O \in \mathcal{O}_\tau(x)$ に対しある $v$ で $w\geq v \implies \varphi(w) \in O$。
Prop VII.6.3: これは $x \in \lim_\tau \varphi[\mathbb{V}]$（$\varphi[\mathbb{V}]$ = 押し出したフィルター基）と同値 — ネットの収束はフィルターの収束に完全に帰着する。列（sequence）はネットの特別な場合（$V=\omega$）。
Mathlib は Filter.Tendsto を基本に据え、ネットは補助概念（Filter.atTop 等）。この本の哲学（フィルター優先）と一致。