# `topology.v` と `derive.v` を読む

- `topology.v`
* フィルターや位相の定義や定理．
* 6349行あり，かなり長い．
- `derive.v`
* 微分に関する諸定理．
* 1607行なので比較的短い．
* `topology.v` に依存している．

## 前提

### フィルタ，生成

$ℱ ⊆ 2^X$ が以下を満たすとき，$ℱ$ は $X$ 上の**フィルタ**であるという：

- $∀F ∈ ℱ. ∀F' ⊆ X. F ⊆ F' ⇒ F' ∈ ℱ$ （つまり包含関係で上に閉じている）
- $∀F_1∀F_2 ∈ ℱ. F_1 ∩ F_2 ∈ ℱ$ （つまり有限個のintersectionについて閉じている）
- $X ∈ ℱ$

$2^X$ を $X$ 上の**自明なフィルタ**といい，自明なフィルタでないフィルタを**真フィルタ**という．

$\mathcal{B} ⊆ 2^X$ に対し，$\mathcal{B}$ を包む最小の（つまり一意的に極小な）フィルタを $\mathcal{B}$ が**生成する**フィルタと呼ぶ．

### 積フィルタ

各 $i ∈ I$ に対して $ℱ_i$ を $X_i$ 上のフィルタとする．このとき，

$$
\left\{ ∏_{i ∈ I} F_i\ \middle|\ (∀i ∈ I. F_i ∈ ℱ_i) ∧ (Иi ∈ I. F_i = X_i)\right\}
$$

が生成する $∏_{i ∈ I} X_i$ 上のフィルタを $\{ℱ_i\}_{i = 1}^{n}$ の**積フィルタ**といい，$∏_{i ∈ I} ℱ_i$ と書く．

ただし，$Иi ∈ I. φ$ は「有限個を除く $I$ の任意の元 $i$ に対して $φ$ が成り立つ」を表す．特に $I$ が有限集合の場合は恒真．

### 位相とフィルタ

位相空間 $T = (X, \mathcal{O})$ および $x ∈ X$ に対し，$N ⊆ X$ が $∃O ∈ \mathcal{O}. x ∈ O ⊆ N$ を満たすとき，$N$ は $x$ の**近傍**であるという．

$x$ の近傍全体はフィルタをなす．実際近傍の定義より明らかに上に閉じており，有限個のintersectionで閉じているのも（位相空間の定義より）有限個の開集合のintersectionがまた開集合であることから簡単にわかる．この近傍全体のフィルタを $x$ の**近傍フィルタ**といい，$R_T(x)$ と書く．

### 真フィルタの極限

$X$ 上のフィルタ $ℱ$ と $ℱ'$ が $ℱ ⊆ ℱ'$ を満たすとき，$ℱ'$ は $ℱ$ より**細かい**という．

位相空間 $T = (X, \mathcal{O})$ に対し，$X$ 上のフィルタ $ℱ$ が $R_T(x)$ よりも細かいとき，つまり $R_T(x) ⊆ ℱ$ のとき，$x$ は $ℱ$ の**極限点**であるという．$ℱ$ の極限点全体を $\lim ℱ$ と書く．

## `topology.v` の冒頭コメントを読む

- `filteredType U`： `U` 上のフィルタ全体に相当する型：

  filteredType U == interface type for types whose
                    elements represent sets of sets on U.
                    These sets are intended to be filters
                    on U but this is not enforced yet.

- `FilteredType U T m`： `T` 型の値を `U` 上のフィルタに `m` によって入射したもの？

  FilteredType U T m == packs the function m: T -> set (set U)
                        to build a filtered type of type
                        filteredType U; T must have a
                        pointedType structure.

  Notation FilteredType U T m := (@pack U T m _ _ idfun).

`@pack` というものがわからないが，とりあえず後回しにする．

- `lim F`： 上記の　$\lim ℱ$．

- `at_point a`： 上記の $R_T(a)$．

- `filter_prod F G`： 上記の $F × G$（$∏$ による直積の2個版）．