長めの例: 中間値の定理

位相のもう 1 つの典型例として，中間値の定理を見ます．

紙の数学では「閉区間 \([a,b]\) は連結であり，連続写像は連結集合を連結集合へ送る． したがって実数値連続関数の像は区間になり，端点値の間の値をすべて取る」と説明します． 数式で書けば，連結な集合 \(s\) 上の連続関数 \(f : X \to \mathbb R\) について， \(a,b \in s\) かつ \(f(a) \le f(b)\) なら

\[ [f(a), f(b)] \subseteq f(s) \]

です． つまり，

\[ f(a) \le c \le f(b) \quad\Longrightarrow\quad \exists x \in s,\ f(x) = c. \]

閉区間版では，\(a \le b\) かつ \(f\) が \([a,b]\) 上連続であれば，

\[ f(a) \le c \le f(b) \quad\Longrightarrow\quad \exists x \in [a,b],\ f(x) = c \]

となります． 端点値の大小が逆なら，\(f(b) \le c \le f(a)\) の形で同じ主張を使います． 前の節で見た IsPreconnected と intermediate_value_Icc を使うと， この議論をそのまま Lean で表せます．

section IntermediateValueTheorem

example {X : Type*} [TopologicalSpace X] {s : Set X} (hs : IsPreconnected s)
    {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f : X → ℝ}
    (hf : ContinuousOn f s) :
    Icc (f a) (f b) ⊆ f '' s := by
  exact hs.intermediate_value ha hb hf

example {X : Type*} [TopologicalSpace X] {s : Set X} (hs : IsPreconnected s)
    {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f : X → ℝ}
    (hf : ContinuousOn f s) {c : ℝ} (hc : c ∈ Icc (f a) (f b)) :
    ∃ x ∈ s, f x = c := by
  rcases hs.intermediate_value ha hb hf hc with ⟨x, hx, hfx⟩
  exact ⟨x, hx, hfx⟩

example {f : ℝ → ℝ} {a b c : ℝ}
    (hab : a ≤ b) (hf : ContinuousOn f (Icc a b))
    (ha : f a ≤ c) (hb : c ≤ f b) :
    ∃ x ∈ Icc a b, f x = c := by
  exact intermediate_value_Icc hab hf ⟨ha, hb⟩

example {f : ℝ → ℝ} {a b c : ℝ}
    (hab : a ≤ b) (hf : ContinuousOn f (Icc a b))
    (ha : f b ≤ c) (hb : c ≤ f a) :
    ∃ x ∈ Icc a b, f x = c := by
  exact intermediate_value_Icc' hab hf ⟨ha, hb⟩

end IntermediateValueTheorem

最後の 2 つの例は，端点値の順序に応じて定理を使い分けています． intermediate_value_Icc は f a ≤ c ≤ f b の場合， intermediate_value_Icc' は f b ≤ c ≤ f a の場合です．

具体例として，\(x^2\) が \([0,2]\) 上で値 \(2\) を取ることを示します． これは平方根の存在そのものではありませんが，中間値の定理の使い方としては典型的です． ここで使っている数学的な事実は，

\[ 0^2 \le 2 \le 2^2 \quad\Longrightarrow\quad \exists x \in [0,2],\ x^2 = 2 \]

です．

example : ∃ x ∈ Icc (0 : ℝ) 2, x ^ 2 = 2 := by
  have hcont : ContinuousOn (fun x : ℝ => x ^ 2) (Icc (0 : ℝ) 2) := by
    exact ((continuous_id : Continuous fun x : ℝ => x).pow 2).continuousOn
  have h2 : (2 : ℝ) ∈ Icc ((fun x : ℝ => x ^ 2) 0) ((fun x : ℝ => x ^ 2) 2) := by
    norm_num
  simpa using intermediate_value_Icc (by norm_num : (0 : ℝ) ≤ 2) hcont h2

Mathlib の証明の読み方

Mathlib の本体では，まず次のような少し強い形を証明しています．

数学的には，連続関数 \(f,g : X \to \mathbb R\) と点 \(a,b \in X\) について

\[ f(a) \le g(a),\qquad g(b) \le f(b) \]

が成り立つなら，

\[ \exists x,\ f(x) = g(x) \]

を示す形です．

intermediate_value_univ₂ :
  Continuous f → Continuous g →
  f a ≤ g a → g b ≤ f b → ∃ x, f x = g x

証明の核だけを抜き出すと次の部分です．

obtain ⟨x, _, hfg, hgf⟩ :
    (univ ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty :=
  isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _
    (isClosed_le hf hg) (isClosed_le hg hf)
    (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩
exact ⟨x, le_antisymm hfg hgf⟩

ここで考える閉集合は

{x | f x ≤ g x},   {x | g x ≤ f x}

です． 数式では

\[ A = \{x \mid f(x) \le g(x)\},\qquad B = \{x \mid g(x) \le f(x)\} \]

と置いています． isClosed_le hf hg によって，連続関数の大小関係で定まる集合が閉集合であることが分かります． また任意の点 x では le_total (f x) (g x) により，少なくともどちらか一方の閉集合に入ります． つまり

\[ X = A \cup B \]

です． 端点の仮定 f a ≤ g a と g b ≤ f b は，それぞれの閉集合が空でないことを与えます．

連結性はここで使われます． isPreconnected_closed_iff は，preconnected な集合を 2 つの閉集合で覆い， 両方に点があるなら，2 つの閉集合の交わりにも点がある，という形の補題です． 数式では，

\[ A \ne \emptyset,\quad B \ne \emptyset,\quad X = A \cup B \quad\Longrightarrow\quad A \cap B \ne \emptyset \]

という使い方です． その交点の点 x では

f x ≤ g x,   g x ≤ f x

が同時に成り立つので，le_antisymm から f x = g x が出ます． すなわち

\[ x \in A \cap B \quad\Longrightarrow\quad f(x) \le g(x)\ \text{and}\ g(x) \le f(x) \quad\Longrightarrow\quad f(x) = g(x). \]

次に，集合 s 上の定理

IsPreconnected.intermediate_value₂

は，s を部分型として見て全空間版を適用します． このとき Subtype.preconnectedSpace hs が「preconnected な集合 s は， 部分型として preconnected な空間になる」ことを与え， continuousOn_iff_continuous_restrict が ContinuousOn f s を 部分型上の Continuous に読み替えます．

最後に，通常の中間値の定理

IsPreconnected.intermediate_value

は，2 つ目の関数 g として定数関数 fun _ => c を取った特殊ケースです． 閉区間版

intermediate_value_Icc

はさらに s = Icc a b とし，isPreconnected_Icc， left_mem_Icc.2 hab，right_mem_Icc.2 hab を渡したものです． 実際の定理の本体はほぼ次の 1 行です．

isPreconnected_Icc.intermediate_value (left_mem_Icc.2 hab) (right_mem_Icc.2 hab) hf

つまり Mathlib の中間値の定理は，

1. 連続関数の大小で定まる閉集合を作る．
2. preconnected 性から，2 つの閉集合の交点を得る．
3. 交点では両向きの不等式があるので等式にする．
4. 一般の集合から閉区間へ特殊化する．

という流れで証明されています．