📐 (VII.2.8)（近傍の入れ子条件）
- 📐 (VII.2.8)（近傍の入れ子条件） #Card
- $\operatorname{int}$ の冪等性 (e) を近傍の言葉に翻訳すると。
$$V \in \mathcal{N}\xi(x) \implies \exists{W \in \mathcal{N}\xi(x)} \forall{w \in W}\ V \in \mathcal{N}_\xi(w). \tag{VII.2.8}$$
「$x$ の近傍 $V$ に対し、$x$ の近傍 $W$ が存在して、$W$ のすべての点にとっても $V$ が近傍になる」。$W := \operatorname{int}_\xi V$ が証拠。
位相の公理を近傍系だけで特徴づける4条件目（他はフィルターであること・$x$ が kernel にあること）。Mathlib の nhds 公理系の核。