Final Convergence $f\xi$ (終収束) (Definition IV.3.5)
- Final Convergence $f\xi$ (終収束) (Definition IV.3.5) #Card
- Given $\xi$ on $X$ and $f : X \to Y$, the finest convergence $\theta$ on $Y$ for which $f \in C(\xi, \theta)$, denoted $f\xi$.
Given a convergence $\xi$ on $X$ and a map $f : X \to Y$, the finest convergence $\theta$ on $Y$, for which $f \in C(\xi, \theta)$, is called the final convergence with respect to $(\xi, f)$, denoted $f\xi$. It always exists (Proposition IV.3.6, $f\xi = \bigvee {\tau : f \in C(\xi, \tau)}$).
- $f$ 全射のとき (IV.3.2): $\lim_{f\xi} \mathcal{G} = \bigcup_{f[\mathcal{F}] \leq \mathcal{G}} f(\lim_\xi \mathcal{F})$；さらに $y \in \lim_{f\xi}\mathcal{G} \iff \exists \mathcal{F}0$ with $\lim\xi \mathcal{F}_0 \cap f^-(y) \neq \emptyset$ and $\mathcal{G} = f[\mathcal{F}_0]$（Prop IV.3.8）。
- $f$ 非全射なら $Y \setminus f(X)$ の各点は $f\xi$-isolated。
- $\xi \geq f^-(f\xi)$（単射なら等号、Prop IV.10.5）。
位相の場合 TopologicalSpace.coinduced f ξ。一般の ConvergenceSpace では Notes/ChapterIV.lean : finalConv（f を連続にする収束すべての交わりとして構成、全射性を仮定しない一般形、lake build 済み）