フィルター

Filter α は，α の部分集合のうち，どれをフィルターに含めるかを指定する構造です． 数学的には，集合 \(X\) 上のフィルター \(\mathcal F\) は，部分集合族 \(\mathcal F \subseteq \mathcal P(X)\) であって，次を満たすものです．

\[ X \in \mathcal F, \qquad A, B \in \mathcal F \Longrightarrow A \cap B \in \mathcal F, \qquad A \in \mathcal F,\ A \subseteq B \subseteq X \Longrightarrow B \in \mathcal F. \]

通常の数学ではさらに \(\emptyset \notin \mathcal F\) も仮定します． Lean の Filter X ではこの条件は定義には入っていませんが， この章で扱う atTop や 𝓝 x を読むうえでは，まず意識しなくてかまいません．

この章では，フィルターの一般論よりも，次の 3 つの読み方が重要です． 型 α 上のフィルター l : Filter α を考えます．

• s ∈ l: s : Set α は α の部分集合であり， s がフィルター l に含まれる，という意味です．
• ∀ᶠ x in l, p x: x : α は集合ではなく，α の点を表す束縛変数です． p : α → Prop に対して，p x が成り立つような点 x 全体の集合が， フィルター l に含まれる，という意味です． 定義上は {x : α | p x} ∈ l という主張です．
• Tendsto f l m: x : α が l に沿って動くとき，f x が m に沿って動く．

数式で書くと，∀ᶠ x in l, p x は

\[ \{x \in X \mid p(x)\} \in \mathcal F \]

という条件です． また，写像 \(f : X \to Y\) とフィルター \(\mathcal F\)，\(\mathcal G\) について Tendsto f l m は，次の条件に対応します．

\[ \forall B \in \mathcal G,\quad f^{-1}(B) \in \mathcal F. \]

この章で主に使うフィルターは，atTop と 𝓝 x です．

atTop は，順序集合の「上の方へ行く」ことを表すフィルターです． 自然数上では「十分大きい n」を意味します． 自然数上の部分集合 \(S \subseteq \mathbb N\) については，

\[ S \in \mathrm{atTop} \quad\Longleftrightarrow\quad \exists N,\ \forall n \ge N,\ n \in S \]

と読めます． この講義では，次の補題を atTop の定義のように読めば十分です．

Mathlib/Order/Filter/AtTopBot/Basic.lean

lemma mem_atTop_sets :
    s ∈ (atTop : Filter α) ↔ ∃ a : α, ∀ b ≥ a, b ∈ s

lemma eventually_atTop :
    (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ b ≥ a, p b

特に自然数列の命題 P : ℕ → Prop について，∀ᶠ m in atTop, P m は 「ある n が存在して，n ≤ m なる任意の m について P m」という意味です． 数式で書けば，

\[ \forall^{\mathrm{eventually}} m,\ P(m) \quad\Longleftrightarrow\quad \exists N,\ \forall m \ge N,\ P(m) \]

です． つまり，有限個の初期項を除けば P m が常に成り立つ，ということです．

一方，𝓝 x は点 x の近傍フィルターです． s ∈ 𝓝 x は，s が x の近傍であることを意味します． 位相空間 \(X\) の点 \(x\) と部分集合 \(S \subseteq X\) については，

\[ S \in \mathcal N(x) \quad\Longleftrightarrow\quad \exists U,\ x \in U,\ U \text{ is open},\ U \subseteq S. \]

実際には，次の補題で読むのが便利です．

Mathlib/Topology/Neighborhoods.lean

theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t

つまり，s が x の近傍であるとは，s の中に x を含む開集合 t があることです．

Tendsto f l m は，「x がフィルター l に沿って動くとき，f x がフィルター m に沿って動く」という意味です． 数列の極限も，関数の一点での極限も，無限遠での極限も，この形で表されます． 内部的には map f l ≤ m という定義ですが，まずは 「m に含まれる任意の集合の逆像は，l に含まれる」と読むのがよいです．

#check Filter
#check Tendsto
#check atTop
#check 𝓝
#check Filter.Eventually
#check mem_atTop_sets
#check eventually_atTop
#check mem_nhds_iff

section Filters

example {α : Type*} {l : Filter α} {p : α → Prop} :
    (∀ᶠ x in l, p x) = ({x | p x} ∈ l) := by
  rfl

example : (∀ᶠ n in (atTop : Filter Nat), 3 ≤ n) := by
  exact eventually_ge_atTop 3

example {P : ℕ → Prop} :
    (∀ᶠ m in (atTop : Filter ℕ), P m) ↔ ∃ n, ∀ m, n ≤ m → P m := by
  exact eventually_atTop

example {s : Set ℕ} :
    s ∈ (atTop : Filter ℕ) ↔ ∃ n, ∀ m, n ≤ m → m ∈ s := by
  exact mem_atTop_sets

example {X : Type*} [TopologicalSpace X] {x : X} {s : Set X} :
    s ∈ 𝓝 x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t := by
  exact mem_nhds_iff

example {α β : Type*} {f : α → β} {l : Filter α} {m : Filter β} :
    Tendsto f l m = (map f l ≤ m) := by
  rfl

end Filters

近傍フィルターで収束と連続を読む

この節で使う対応は次の 2 つです．

\[ \mathcal N(x) = \text{the neighborhood filter of } x, \]

すなわち

\[ A \in \mathcal N(x) \quad\Longleftrightarrow\quad \exists U,\ x \in U,\ U \text{ is open},\ U \subseteq A. \]

また，写像 \(f : X \to Y\) について

\[ \operatorname{Tendsto}(f,\mathcal F,\mathcal G) \quad\Longleftrightarrow\quad \forall B \in \mathcal G,\ f^{-1}(B) \in \mathcal F. \]

点列 u : ℕ → X が x に収束することは，次のように書きます．

Tendsto u atTop (𝓝 x)

これは数式では，

\[ \operatorname{Tendsto}(u,\mathrm{atTop},\mathcal N(x)) \quad\Longleftrightarrow\quad \forall A \in \mathcal N(x),\ \{n \in \mathbb N \mid u_n \in A\} \in \mathrm{atTop} \]

です． さらに，\(\mathrm{atTop}\) を

\[ S \in \mathrm{atTop} \quad\Longleftrightarrow\quad \exists N,\ \forall n \ge N,\ n \in S \]

と読むと，これは通常の点列収束

\[ u_n \to x \quad\Longleftrightarrow\quad \forall U, \bigl(U \text{ is open} \land x \in U\bigr) \Longrightarrow \exists N,\ \forall n \ge N,\ u_n \in U \]

と同じです． tendsto_nhds は，この条件を開集合で読むための補題です．

Mathlib/Topology/Neighborhoods.lean

theorem tendsto_nhds {a : X} {f : α → X} {l : Filter α} :
    Tendsto f l (𝓝 a) ↔
      ∀ s, IsOpen s → a ∈ s → f ⁻¹' s ∈ l

対応する証明は，次の式変形として読めます．

まず \(U\) が \(x\) を含む開集合なら

\[ x \in U,\ U \text{ is open} \quad\Longrightarrow\quad U \in \mathcal N(x). \]

したがって

\[ \operatorname{Tendsto}(u,\mathrm{atTop},\mathcal N(x)) \quad\Longrightarrow\quad u^{-1}(U) \in \mathrm{atTop} \quad\Longleftrightarrow\quad \exists N,\ \forall n \ge N,\ u_n \in U. \]

逆向きでは，任意の \(A \in \mathcal N(x)\) に対して

\[ A \in \mathcal N(x) \quad\Longrightarrow\quad \exists U,\ x \in U,\ U \text{ is open},\ U \subseteq A. \]

仮定より

\[ \exists N,\ \forall n \ge N,\ u_n \in U. \]

\(U \subseteq A\) なので

\[ \exists N,\ \forall n \ge N,\ u_n \in A, \]

すなわち

\[ u^{-1}(A) \in \mathrm{atTop}. \]

一点 x での連続性も，同じ Tendsto で定義されます．

Mathlib/Topology/Defs/Filter.lean

def ContinuousAt (f : X → Y) (x : X) :=
  Tendsto f (𝓝 x) (𝓝 (f x))

数式では，

\[ f \text{ is continuous at } x \quad\Longleftrightarrow\quad \forall V \in \mathcal N(f(x)),\ f^{-1}(V) \in \mathcal N(x) \]

です． 開集合で書けば，

\[ f \text{ is continuous at } x \quad\Longleftrightarrow\quad \forall V, \bigl(V \text{ is open} \land f(x) \in V\bigr) \Longrightarrow \exists U,\ x \in U,\ U \text{ is open},\ U \subseteq f^{-1}(V). \]

大域的な連続性は，次の補題により「開集合の逆像が開集合」と同値になります． すなわち，

\[ f \text{ is continuous} \quad\Longleftrightarrow\quad \forall V \subseteq Y, V \text{ is open} \Longrightarrow f^{-1}(V) \text{ is open}. \]

Mathlib/Topology/Continuous.lean

theorem continuous_def :
    Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s)

theorem continuous_iff_continuousAt :
    Continuous f ↔ ∀ x, ContinuousAt f x

この同値性の証明も，近傍の式で追えます． 各点で

\[ \forall x,\ \forall A \in \mathcal N(f(x)),\ f^{-1}(A) \in \mathcal N(x) \]

が成り立つとします． \(V \subseteq Y\) が開集合なら，

\[ x \in f^{-1}(V) \quad\Longrightarrow\quad f(x) \in V \quad\Longrightarrow\quad V \in \mathcal N(f(x)). \]

よって

\[ f^{-1}(V) \in \mathcal N(x) \qquad (x \in f^{-1}(V)). \]

任意の点 \(x \in f^{-1}(V)\) で \(f^{-1}(V)\) が \(x\) の近傍なので，

\[ f^{-1}(V) \text{ is open}. \]

逆に，

\[ \forall V \subseteq Y, V \text{ is open} \Longrightarrow f^{-1}(V) \text{ is open} \]

を仮定します． \(A \in \mathcal N(f(x))\) なら

\[ \exists V,\ f(x) \in V,\ V \text{ is open},\ V \subseteq A. \]

このとき

\[ x \in f^{-1}(V),\qquad f^{-1}(V) \text{ is open},\qquad f^{-1}(V) \subseteq f^{-1}(A). \]

したがって

\[ f^{-1}(A) \in \mathcal N(x). \]

これは

\[ \operatorname{Tendsto}(f,\mathcal N(x),\mathcal N(f(x))) \]

です．

#check tendsto_nhds
#check continuous_def
#check continuous_iff_continuousAt

section NeighborhoodFilters

example {X : Type*} [TopologicalSpace X] (x : X) : Filter X :=
  𝓝 x

example {X : Type*} [TopologicalSpace X] {u : ℕ → X} {U : Set X} :
    (u ⁻¹' U ∈ atTop) = (∀ᶠ n in atTop, u n ∈ U) := by
  rfl

example {X : Type*} [TopologicalSpace X] (u : ℕ → X) (x : X) :
    Tendsto u atTop (𝓝 x) ↔
      ∀ U : Set X, IsOpen U → x ∈ U → ∀ᶠ n in atTop, u n ∈ U := by
  exact tendsto_nhds

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} {x : X} :
    ContinuousAt f x = Tendsto f (𝓝 x) (𝓝 (f x)) := by
  rfl

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} :
    Continuous f ↔ ∀ x, Tendsto f (𝓝 x) (𝓝 (f x)) := by
  simpa [ContinuousAt] using (continuous_iff_continuousAt (f := f))

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} :
    Continuous f ↔ ∀ U : Set Y, IsOpen U → IsOpen (f ⁻¹' U) := by
  exact continuous_def

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} :
    (∀ x, Tendsto f (𝓝 x) (𝓝 (f x))) ↔
      ∀ U : Set Y, IsOpen U → IsOpen (f ⁻¹' U) := by
  rw [← continuous_def]
  simpa [ContinuousAt] using (continuous_iff_continuousAt (f := f)).symm

end NeighborhoodFilters

演習問題

Tendsto の定義を map と filter の順序として読み替えてください．

example {α β : Type*} (f : α → β) (l : Filter α) (m : Filter β) :
    Tendsto f l m = (map f l ≤ m) := by
  -- 定義そのもの．
  -- 解答例: rfl
  sorry