Neighborhood Filter Properties

• Neighborhood Filter Properties #Card
  • • Isotone (単調性): $W \supset V \in \mathcal{N}(x) \implies W \in \mathcal{N}(x)$ - Finitely Complete (有限交差性): $V_0, V_1 \in \mathcal{N}(x) \implies V_0 \cap V_1 \in \mathcal{N}(x)$ - Proper (固有性): $\emptyset \notin \mathcal{N}(x)$

Back

• Isotone (単調性): $W \supset V \in \mathcal{N}(x) \implies W \in \mathcal{N}(x)$
• Finitely Complete (有限交差性): $V_0, V_1 \in \mathcal{N}(x) \implies V_0 \cap V_1 \in \mathcal{N}(x)$
• Proper (固有性): $\emptyset \notin \mathcal{N}(x)$

Lean

Filter 公理（nhds が満たす isotone/finite-intersection）