Corollary II.1.2 (部分列の収束)
- Corollary II.1.2 (部分列の収束) #Card
- 列が $x$ に収束するとき、その部分列は？
If a sequence $\varphi$ converges to $x$ and $\psi$ is a subsequence of $\varphi$, then $\psi$ converges to $x$.
（土台は (II.1.2): $\psi$ が $\varphi$ の部分列なら $\Gamma_\varphi \subset \Gamma_\psi$。よって $\mathcal{N}(x) \subset \Gamma_\varphi \subset \Gamma_\psi$——フィルターの包含だけで従う。）
Filter.Tendsto.comp（StrictMono.tendsto_atTop と合成）
本ノート RoyalRoad.ChapterII.cor_II_1_2（Notes/ChapterII.lean、lake build 済み）