跳轉到

3.3 函數：Injective 與 Surjective#

本節目標#

  • 把「函數即映射」的直覺翻譯成 Lean 的型別世界。
  • 掌握 Function.Injective、Function.Surjective、Function.Bijective 的 Mathlib 定義。
  • 完整證明範例： \(f(x) = 2x+1\) 是從 \(\mathbb{Z}\) 到 \(\mathbb{Z}\) 的 bijection。
  • 學會 Function.LeftInverse 與反函數存在性的直覺。
  • 熟悉 Function.Injective 的 ∀ a b, f a = f b → a = b 展開與 tactic 套路。

函數即映射#

在型別論中，函數是「型別之間的映射」：f : α → β 把每個 a : α 唯一對應到一個 b : β。 這正是函數的集合論定義「滿足唯一性條件的關係」的直接體現—— 唯一性在型別論中是免費的（一個項只有一個值），所以 Lean 的函數概念反而比樸素集合論更乾淨。

常見的集合論概念在 Lean 中的對應：

  • 定義域／對應域：α / β（是型別，不是集合）。
  • 值域：Set.range f = {y | ∃ x, f x = y}。
  • 像與原像：Set.image f s = {y | ∃ x ∈ s, f x = y}、Set.preimage f t = {x | f x ∈ t}。

三個關鍵定義#

Mathlib 中的定義（簡化後）：

def Function.Injective (f : α → β) : Prop :=
  ∀ a b, f a = f b → a = b

def Function.Surjective (f : α → β) : Prop :=
  ∀ b, ∃ a, f a = b

def Function.Bijective (f : α → β) : Prop :=
  f.Injective ∧ f.Surjective

用數學符號寫：

\[ \text{Injective}(f) \iff \forall a\, b,\; f(a) = f(b) \to a = b \]
\[ \text{Surjective}(f) \iff \forall b,\; \exists a,\; f(a) = b \]

單射的直覺：不同的輸入給不同的輸出（用「輸出相同則輸入相同」表述，方便證明）。 滿射的直覺：每個輸出都有人負責。

Function.Injective 的展開與 tactic 套路#

目標 Function.Injective f 展開後是 ∀ a b, f a = f b → a = b。 標準套路：

example (f : ℕ → ℕ) (hf : ∀ x, f (x + 1) = f x + 1) : Function.Injective f := by
  intro a b hab            -- 拆掉 ∀ a b
  -- hab : f a = f b，目標 a = b
  ...

實戰技巧：

  • intro a b hab 之後，hab : f a = f b 就是我們的「假設彈藥」。
  • 若 f 是由具體算術構成（如 2 * x + 1），用 simp / omega 消化等式。
  • 反向使用單射：有 hf : Function.Injective f 且 hab : f a = f b 時， hf hab : a = b——把假設當函數套用，這是 Lean 風格的精妙之處。
  • Function.Injective.eq_iff : 對單射 \(f\) ， \(f a = f b \iff a = b\) 。

範例： \(f(x) = 2x + 1\) 是 \(\mathbb{Z} \to \mathbb{Z}\) 的 bijection#

先證單射：

def f : ℤ → ℤ := fun x => 2 * x + 1

theorem f_injective : Function.Injective f := by
  intro a b hab
  simp only [f] at hab
  -- hab : 2 * a + 1 = 2 * b + 1
  omega

omega 是線性算術的自動證明器，一拿到 2 * a + 1 = 2 * b + 1 就能推出 a = b（它會先消去常數項再除以 2——不過是在整數上，安全）。

再證滿射：對任意 \(y\) ，取 \(a = \frac{y-1}{2}\) 即可。 在 \(\mathbb{Z}\) 上這個除法是良定義的（ \(y - 1\) 必為偶數，因為 \(y = 2a+1\) 的候選）。 直接構造：

theorem f_surjective : Function.Surjective f := by
  intro y
  refine ⟨(y - 1) / 2, ?_⟩
  simp only [f]
  have : y - 1 = 2 * ((y - 1) / 2) := by omega
  omega

合併：

theorem f_bijective : Function.Bijective f :=
  ⟨f_injective, f_surjective⟩

注意若把同樣的 \(f\) 視為 \(\mathbb{N} \to \mathbb{N}\) ，它就不是滿射： \(0\) 沒有原像（ \(2x+1 \geq 1\) ）。這提醒我們：單射、滿射是 函數連同其型別的性質，換了定義域或對應域，結論可能改變。

合成函數的性質#

設 \(g \circ f\) 表示先 \(f\) 後 \(g\) ：

  • 若 \(f, g\) 都是單射，則 \(g \circ f\) 是單射。
  • 若 \(f, g\) 都是滿射，則 \(g \circ f\) 是滿射。

Mathlib 中有現成引理：Function.Injective.comp、Function.Surjective.comp。 手動證明單射版本，練習套路：

example {f : α → β} {g : β → γ}
    (hf : Function.Injective f) (hg : Function.Injective g) :
    Function.Injective (g ∘ f) := by
  intro a b hab
  -- hab : g (f a) = g (f b)
  apply hf
  apply hg
  exact hab

兩個 apply 各自「消掉一層函數」，最後剩下的等式正是 hab。 滿射版本用 obtain 取見證：

example {f : α → β} {g : β → γ}
    (hf : Function.Surjective f) (hg : Function.Surjective g) :
    Function.Surjective (g ∘ f) := by
  intro c
  obtain ⟨b, hb⟩ := hg c
  obtain ⟨a, ha⟩ := hf b
  exact ⟨a, by simp [ha, hb]⟩

Function.LeftInverse 與反函數#

定義：

def Function.LeftInverse (g : β → α) (f : α → β) : Prop :=
  ∀ x, g (f x) = x

\(g\) 是 \(f\) 的左反函數，意思是 \(g \circ f = \mathrm{id}\) 。 對偶地有 Function.RightInverse g f := LeftInverse f g。

三者關係（皆有 Mathlib 引理）：

  • Function.LeftInverse.injective：有左反函數則單射。
  • Function.RightInverse.surjective：有右反函數則滿射。
  • Function.LeftInverse.comp_right 等合成版本。

回到範例： \(f(x) = 2x+1\) 的反函數是 \(g(y) = \frac{y-1}{2}\) ：

example : Function.LeftInverse (fun y => (y - 1) / 2) f := by
  intro x
  simp only [f]
  omega

反函數存在性直覺： \(f : \alpha \to \beta\) 有反函數 \(\iff\) \(f\) 是雙射（在選擇公理成立的前提下）。 單射保證「往回走不會歧義」，滿射保證「每個 \(b\) 都走得回去」， 合起來恰好定義 \(f^{-1}\) 。在 Lean 中這依賴 Classical.choice， Mathlib 的 Function.Bijective.of_comp_iff 系列以及 Function.surjective_to_leftInverse（滿射 + 選擇 → 右反）體現了這件事。

小結與練習#

單射、滿射都是逐點的全稱／存在命題， 套路分別是「intro + 用假設推等式」與「intro + 構造見證 refine ⟨_, _⟩」。 LeftInverse 把「有反函數」變成可操作的假設， 是日後討論等勢（第三章之後）的基礎。

練習：

  1. 證明 f(x) = 2x + 1 : ℕ → ℕ 是單射但不是滿射 （後半提示：用 obtain 對 0 的原像做情況分析）。
  2. 證明：Function.Injective f → Function.Injective (fun x => f x + 1)（對 f : ℤ → ℤ）。
  3. 證明合成滿射版本 Function.Surjective.comp 的內容（不用現成引理）。
  4. 證明：若 g 是 f 的左反函數且 f 是 g 的左反函數， 則 f 是雙射。提示：Function.LeftInverse.injective 與 左右反的對偶性。
  5. 證明：常數函數 fun _ => 0 : α → ℕ 在 α 至少有兩個元素時不單射。