📐 Proposition IV.3.5（随伴公式：連続性 = 始収束 = 終収束）
- 📐 Proposition IV.3.5（随伴公式：連続性 = 始収束 = 終収束） #Card
- 終収束 $f\xi$・連続性 $f\in C(\xi,\tau)$・始収束 $f^-\tau$ の3条件が同値であることの主張は。
$$f\xi \geq \tau \iff f \in C(\xi,\tau) \iff \xi \geq f^-\tau. \tag{IV.3.5}$$
（cards/topology/final-convergence・cards/topology/initial-convergence を仲立ちにした、連続写像の集合 $C(\xi,\tau)$ を軸にした Galois 接続。）著者自身が「very, very useful formula!」と強調する、第IV章全体の背骨（始収束・終収束・積・商・埋め込みがすべてこの一本から出る）。
位相の場合の対応: Mathlib gc_coinduced_induced（TopologicalSpace.coinduced・TopologicalSpace.induced の Galois 接続）。
Notes/ChapterIV.lean : prop_IV_3_5（一般の ConvergenceSpace で形式化。終収束 finalConv は「f を連続にする収束すべての交わり」として構成し全射性を仮定しない一般形。TFAE で3条件の同値を証明、lake build 済み）