Chapter 03: 位相

Mathlib における基本的な位相を扱います．

参考:

• Mathematics in Lean, 11. Topology: https://leanprover-community.github.io/mathematics_in_lean/C11_Topology.html
• Maths in Lean: Topological, uniform and metric spaces: https://leanprover-community.github.io/theories/topology.html

フィルター，距離空間，位相空間，連続性，コンパクト性などが説明されています．

Lean での位相はフィルターに基づいて形式化されています． フィルターは，数列の極限，関数の極限，無限遠での振る舞い，近傍などを同じ言葉で扱うための道具です．

import Mathlib

namespace PracticeChapter03

open Set Filter
open scoped Topology