Proposition IV.3.15 (連続性の随伴公式・最重要)
- Proposition IV.3.15 (連続性の随伴公式・最重要) #Card
- $f\xi$, $C(\xi,\tau)$, $f^-\tau$ を結ぶ「very, very useful formula」。
The following statements are equivalent: $$f\xi \geq \tau \iff f \in C(\xi, \tau) \iff \xi \geq f^-\tau. \tag{IV.3.5}$$
- 連続性を不等式の操作に変える公式。本書全体で頻用される（著者曰く “very, very useful formula!”）。
- 帰結: $f(f^-\tau) \geq \tau$（全射で等号）、$\xi \geq f^-(f\xi)$（単射で等号）。
- $\xi \approx \tau \iff \exists f$ bijective with $\xi = f^-\tau \iff f\xi = \tau$。
証明の骨子. 二つの同値は終収束・始収束の定義そのものから直ちに従う（それぞれが $C(\xi,\tau)$ 上の Galois 接続の左随伴・右随伴）。
- $f\xi \geq \tau \iff f \in C(\xi,\tau)$: 終収束 $f\xi$ は「$\xi$ から $f$ を連続にする最も細かい（finest）収束」（cards/topology/final-convergence、Prop IV.3.6）。ある収束 $\tau$ について $f\xi \geq \tau$ とは、$f$ が $\xi \to \tau$ で連続にできる収束のうち $\tau$ が下限側にあること、すなわち $f \in C(\xi,\tau)$ に他ならない（$f\xi$ の普遍性）。
- $f \in C(\xi,\tau) \iff \xi \geq f^-\tau$: 始収束 $f^-\tau$ は「$f$ を $\tau$ へ連続にする最も粗い（coarsest）収束」（cards/topology/initial-convergence）。$\xi \geq f^-\tau$ とは $\xi$ がその粗い収束より細かいこと、すなわち $f$ が $\xi \to \tau$ で連続になることに他ならない。Lean では
Notes/ChapterIV.lean : prop_IV_3_5がfinalConv／initialConvを明示構成して TFAE で形式化済み（cards/topology/prop-iv-3-5 と同一公式）。 - 帰結: $f \in C(f^-\tau,\tau)$ より $f(f^-\tau) \geq \tau$ (IV.3.6)、$f \in C(\xi,f\xi)$ より $\xi \geq f^-(f\xi)$ (IV.3.7)。全射／単射で等号（Prop IV.10.5/10.6）。∎
位相の場合 coinduced f ξ ≤ τ ↔ Continuous f ↔ ξ ≤ induced f τ（continuous_iff_coinduced_le / continuous_iff_le_induced；Galois 接続 gc_coinduced_induced）