Pretopology (前位相) (Definition III.1.10)
- Pretopology (前位相) (Definition III.1.10) #Card
- A convergence $\xi$ is called a pretopology if $\xi^-(x)$ has a coarsest filter for each $x \in |\xi|$.
A convergence $\xi$ is called a pretopology if $\xi^-(x)$ has a coarsest filter for each $x \in |\xi|$.
- Equivalently: $x \in \lim_\xi V_\xi(x)$ for each $x$（cards/topology/prop-iii-1-11）; the coarsest filter converging to $x$ is then the vicinity filter $V_\xi(x)$.
- Equivalently: at each point there is a pavement consisting of one filter（cards/topology/prop-iii-2-3）.
- $\iota$, $o$, $\nu_\mathbb{R}$ are pretopologies; $\sigma_\mathbb{R}$ is not.
Meaning
Section titled “Meaning”収束 $\xi$ が pretopology とは、各点 $x$ について $\xi^-(x)$（$x$ に $\xi$-収束する filter の集合）が coarsest filter を持つことである。Proposition III.1.11 により、これは各 $x$ について $x \in \lim_\xi V_\xi(x)$ と同値——近傍系 filter 自身が $x$ に収束する。
離散・混沌・標準収束 $\nu_\mathbb{R}$ は pretopology。標準列型収束 $\sigma_\mathbb{R}$ は pretopology ではない（Example III.1.9）。位相（第VII章）は pretopology のさらに特別な場合として現れる。
出典:
refs/math/topology/royal-road-to-topology/pdfs/chp3-2024-convergence-of-filters.pdfp.37–38
Notes/ChapterIII.lean : IsPretopology（∃ V, IsGreatest (ConvergentFilters ξ x) V、ConvergentFilters = proper filter で x に収束するもの全体、lake build 済み）