まとめ

Mathlib の位相では，極限を直接 ε-δ で定義するのではなく，フィルター Tendsto を基礎にします． 開集合・閉集合・閉包・内部は Set 上の述語や操作として扱われます． 距離空間では Metric.ball や dist を使い，連続性は Continuous，ContinuousAt，ContinuousOn で表します． 特に ContinuousAt f x は Tendsto f (𝓝 x) (𝓝 (f x)) なので，点での連続性もフィルターの極限として読めます． 中間値の定理では，閉区間 Icc a b が IsPreconnected であることと， 連続関数の大小関係で定まる閉集合が閉じていることを組み合わせます．

微分と積分の章では，これらの位相的な語彙がそのまま使われます．

形式化の tips

位相の形式化では，同じ定理が「集合の言葉」「フィルターの言葉」「距離の言葉」で出てきます． どのレベルで証明するかを選ぶのが重要です．

1. 開集合・閉集合の問題なら IsOpen，IsClosed を探す．
2. 極限の問題なら Tendsto と 𝓝 を読む．
3. 距離空間の問題なら Metric.ball，dist，Metric.mem_ball を使う．
4. 連続性の合成なら Continuous.comp または hg.comp hf を使う．
5. compactness では，Hausdorff 条件 [T2Space X] が必要かを確認する．
6. 中間値の定理では intermediate_value_Icc と intermediate_value_Icc' を探す．