# 定義域、陪域與值域：有限表格與 h(x)=x²+1 的值域

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-domain-codomain-range/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-domain-codomain-range-01 · production-20261019-adopted-96



## 目標與範圍

(1) 設 A={−1,0,1,2}、B={0,1,2,3,4,5}、f(x)=x²+1：驗證 f:A→B 是總函數，求值域 f[A]，並說明 f[A]⊆B 但 f[A]≠B；(2) 說明輸出落在宣告陪域外或漏掉輸入的資料不是本條目的總函數；(3) 對 h:ℝ→ℝ、h(x)=x²+1，證明值域是 [1,∞)，不等於陪域 ℝ。

在 MKO 的範圍內：明示 A、B 的總函數（假設 a1）。實數部分只用平方非負與主平方根的存在。不處理部分函數、反函數、集合論基礎或一般的值域求法；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- function_def
- image_preimage_def
- set_extensionality
- subset_def
- square_nonneg
- sqrt_def
- order_basics
- numeric_evaluation


- G1 — A={−1,0,1,2}，B={0,1,2,3,4,5}，對 x∈A 令 f(x)=x²+1；宣告的函數是 f:A→B。
- G2 — h:ℝ→ℝ，h(x)=x²+1。
- G3 — 函數資料包含定義域、陪域與對應規則三者（MKO 假設 a1：A、B 已明示）。


- A,\ B — 定義域與陪域
- f[A] — 值域 {f(x) ∣ x∈A}
- h — 實函數 h(x)=x²+1
- [1,\infty) — {y∈ℝ ∣ y≥1}
- \sqrt{u} — u≥0 的主平方根





## 規則與來源


- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- image_preimage_def · prerequisite — 像與原像：f(S)={f(a) ∣ a∈S}；f⁻¹(T)={a∈A ∣ f(a)∈T}。原像記號不預設 f 有反函數。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- injective_surjective_def · prerequisite — 單射：f(a)=f(a′) ⇒ a=a′。滿射：每個 b∈B 都有 a∈A 使 f(a)=b。雙射：既單又滿，此時有唯一反函數 f⁻¹ 使 f⁻¹∘f=id_A、f∘f⁻¹=id_B。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_dcr_def · cited — 對總函數 f:A→B，A 是允許的全部輸入，B 是宣告的輸出集合；值域 f[A]={f(x):x∈A} 是 B 的子集合，未必等於 B。 · mko-domain-codomain-range
- interval_def · prerequisite — [1,∞)={y∈ℝ ∣ y≥1}。
- L_range_sub · lemma — 對任何總函數 f:A→B，f[A]⊆B。
- L_shift · lemma — 對實數 u：u≥0 ⇔ u+1≥1。





## 逐步主鏈

S01 · definition操作前

f:A\to B

操作後

\text{domain}\ A,\ \text{codomain}\ B,\ f[A]=\{f(x)\mid x\in A\}

條件：無

規則：mko_dcr_def · 依賴：G3, mko_dcr_def

葉節點依據：mko_dcr_def + image_preimage_def

依 MKO：定義域 A 是允許的全部輸入，陪域 B 是宣告的輸出集合，值域 f[A] 只收集實際出現的輸出。三者是不同的東西：A、B 是宣告的一部分，f[A] 要計算出來。



S02 · implies操作前

f(x)=x^2+1,\ x\in A

操作後

f(-1)=2,\ f(0)=1,\ f(1)=2,\ f(2)=5

條件：無

規則：numeric_evaluation · 依賴：G1

葉節點依據：numeric_evaluation + power_laws

逐一計算 A 的四個輸入：(−1)²+1=2，0²+1=1，1²+1=2，2²+1=5。每個輸入代入規則恰得一個數。



S03 · implies操作前

f(-1)=2,\ f(0)=1,\ f(1)=2,\ f(2)=5

操作後

f:A\to B\ \text{is a total function}

條件：無

規則：function_def · 依賴：G1, S02, function_def

葉節點依據：function_def + set_builder

總函數要求：A 的每個輸入都有輸出、每個輸入恰有一個輸出、輸出都在 B 中。S02 對四個輸入各給出一個值；2、1、2、5 都屬於 B={0,1,2,3,4,5}。所以 f:A→B 是總函數。



S04 · equivalent操作前

f[A]=\{f(-1),f(0),f(1),f(2)\}

操作後

f[A]=\{2,1,2,5\}=\{1,2,5\}

條件：無

規則：set_extensionality · 依賴：S01, S02, set_extensionality

葉節點依據：set_extensionality + image_preimage_def + eq_replace

依定義，值域是所有 f(x)（x∈A）組成的集合。代入 S02 的值得 {2,1,2,5}。集合只看有哪些元素，重複的 2 只算一次，順序也不重要，所以 f[A]={1,2,5}，有 3 個元素。



S05 · theorem_application操作前

f[A]=\{1,2,5\}

操作後

f[A]\subseteq B

條件：無

規則：L_range_sub · 依賴：S03, S04, L_range_sub

葉節點依據：L_range_sub + subset_def

依引理 L_range_sub，總函數的值域一定是陪域的子集合；本例也可直接看到 1、2、5 都在 B 中。



S06 · implies操作前

f[A]=\{1,2,5\},\ B=\{0,1,2,3,4,5\}

操作後

0\in B\setminus f[A],\ \text{so}\ f[A]\neq B;\ B\setminus f[A]=\{0,3,4\}

條件：無

規則：set_extensionality · 依賴：G1, S04

葉節點依據：set_extensionality + set_operations_def

0 屬於 B，但 0 不是 1、2、5 中的任何一個，所以 0∉f[A]。兩個集合元素不同，依外延原則 f[A]≠B。同理 3、4 也在 B 中而不在值域中：B∖f[A]={0,3,4}。這就是 MKO 所說「值域未必等於 B」。



S07 · implies操作前

\text{rule}\ x^2+1\ \text{declared as}\ A\to B'=\{0,1,2,3,4\}

操作後

f(2)=5\notin B':\ \text{not a total function}\ A\to B'

條件：無

規則：function_def · 依賴：S02, function_def

葉節點依據：function_def + numeric_evaluation

非實例一：同一規則若宣告陪域為 B′={0,1,2,3,4}，則輸入 2 的輸出 5 不在 B′ 中，違反「輸出必須落在陪域」，所以這份宣告不是總函數 A→B′。不能為了遷就輸出而事後擴大或忽略陪域。



S08 · implies操作前

\text{table}\ \{(-1,2),(0,1),(1,2)\}\ \text{claimed as a function on}\ A

操作後

2\in A\ \text{has no output: not total on}\ A

條件：無

規則：function_def · 依賴：G1, function_def

葉節點依據：function_def

非實例二：只列出 −1、0、1 三個輸入的表格，被宣稱為 A 上的函數。但 2∈A 沒有輸出，違反「A 的每個輸入都有輸出」。用這張表算出的 {1,2} 不是 f[A]；它漏掉了 5。MKO 指出，不能以有未定義輸入的表格計算宣稱的總函數的值域。



S09 · implies操作前

f_C:A\to C=\{1,2,5\},\ f_C(x)=x^2+1

操作後

f_C\neq f\ \text{as function data},\ f_C[A]=\{1,2,5\}=C

條件：無

規則：function_def · 依賴：S02, S04, function_def

葉節點依據：function_def + injective_surjective_def

同樣的規則改宣告陪域 C={1,2,5}：每個輸出 1、2、5 都在 C 中，所以 f_C:A→C 是總函數。依 function_def，兩個函數相等需要定義域、陪域都相同，而 B≠C，所以 f_C 與 f 是不同的函數資料，儘管值域都是 {1,2,5}。對 f_C 而言值域等於陪域（滿射），對 f 則不是。



S10 · implies操作前

x\in\mathbb{R}

操作後

h(x)=x^2+1\geq 1,\ \text{so}\ h[\mathbb{R}]\subseteq[1,\infty)

條件：無

規則：L_shift · 依賴：G2, square_nonneg, L_shift

葉節點依據：square_nonneg + L_shift + subset_def + forall_intro

h 在每個實數都有唯一的實數值 x²+1，所以 h:ℝ→ℝ 是總函數。任取 x∈ℝ：依 square_nonneg，x²≥0；依引理 L_shift（u=x²），x²+1≥1。所以每個輸出都在 [1,∞) 中，即 h[ℝ]⊆[1,∞)。



S11 · implies操作前

y\in[1,\infty)

操作後

y-1\geq 0,\ \ t=\sqrt{y-1}\in\mathbb{R},\ \ t^2=y-1

條件：y-1\geq 0

規則：sqrt_def · 依賴：L_shift, sqrt_def, interval_def

葉節點依據：sqrt_def + L_shift + interval_def

任取 y∈[1,∞)，即 y≥1。依 L_shift（u=y−1，且 (y−1)+1=y），y−1≥0。非負實數有主平方根，所以 t=√(y−1) 是實數且 t²=y−1。



S12 · implies操作前

t^2=y-1

操作後

h(t)=(y-1)+1=y,\ \text{so}\ y\in h[\mathbb{R}]

條件：無

規則：image_preimage_def · 依賴：G2, S11, image_preimage_def

葉節點依據：image_preimage_def + exists_intro + forall_intro + eq_replace

h(t)=t²+1=(y−1)+1=y。t 是實數，所以 y 是某個輸入的輸出，依值域定義 y∈h[ℝ]。y 是 [1,∞) 中任意的元素，所以 [1,∞)⊆h[ℝ]。例如 y=10 時 t=√9=3，h(3)=10。



S13 · implies操作前

h[\mathbb{R}]\subseteq[1,\infty),\ [1,\infty)\subseteq h[\mathbb{R}]

操作後

h[\mathbb{R}]=[1,\infty)

條件：無

規則：set_extensionality · 依賴：S10, S12, set_extensionality

葉節點依據：set_extensionality

兩個方向的包含都已證明（S10、S12），依外延原則 h[ℝ]=[1,∞)。



S14 · implies操作前

h[\mathbb{R}]=[1,\infty)

操作後

0\in\mathbb{R}\setminus h[\mathbb{R}],\ \text{so}\ h[\mathbb{R}]\neq\mathbb{R}

條件：無

規則：set_extensionality · 依賴：S13, interval_def

葉節點依據：set_extensionality + interval_def + order_basics

0 是實數，但 0<1，所以 0∉[1,∞)=h[ℝ]；也就是方程 x²+1=0 沒有實數解。陪域 ℝ 與值域 [1,∞) 元素不同，所以不相等：宣告的陪域 ℝ 並不是實際輸出的集合。



S15 · implies操作前

S03\ \text{to}\ S08,\ S13,\ S14

操作後

f[A]=\{1,2,5\}\subsetneq B;\ \ h[\mathbb{R}]=[1,\infty)\neq\mathbb{R}

條件：無

規則：and_intro_elim · 依賴：S03, S04, S05, S06, S07, S08, S13, S14

葉節點依據：and_intro_elim

目標 (1) 由 S03 到 S06 完成，(2) 由 S07、S08 完成，(3) 由 S13、S14 完成。







## 局部子步與引理

S05.1 · implies操作前

y\in f[A]

操作後

y\in B

條件：無

規則：subset_def · 依賴：image_preimage_def, function_def, subset_def

葉節點依據：image_preimage_def + function_def + subset_def + exists_elim + forall_intro

任取 y∈f[A]。依值域的定義，存在 x∈A 使 y=f(x)（取這個 x 為新名字）。f 是 A→B 的總函數，所以 f(x)∈B，因此 y∈B。y 是任意的，依子集定義 f[A]⊆B。此子步證得引理 L_range_sub。



S10.1 · equivalent操作前

u\geq 0

操作後

u+1\geq 1

條件：無

規則：order_basics · 依賴：order_basics

葉節點依據：order_basics + add_inverse + add_assoc + add_zero

⇒：兩邊同加 1（u>0 時嚴格不等號保持，u=0 時得 1=1）。⇐：兩邊同加 −1，(u+1)+(−1)=u，1+(−1)=0。此子步證得引理 L_shift。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S03, S04, S05, S06, S07, S08, S13, S14, and_intro_elim — 目標 G：(1) 到 (3)。足夠條件 H：所列各步成立；H⇒G 由合取引入。H 由定義、引理與計算正向證成，沒有把 G 當作前提。
- S14 · premise_audit · S13, interval_def, order_basics — 一個在陪域中而不在值域中的元素就足以說明兩者不等。
- S13 · premise_audit · S10, S12, set_extensionality — 集合相等需要兩個方向；只有 S10 只能說值域包含於 [1,∞)。
- S12 · premise_audit · S11, image_preimage_def, exists_intro, forall_intro — 每個 y 只需找到一個輸入；不宣稱輸入唯一（−t 也給出 y）。
- S11 · premise_audit · L_shift, sqrt_def — 開平方需要 y−1≥0；若 y<1，y−1<0 在實數中沒有平方根，這正對應 y 不在值域中。
- S10.1 · inverse_equivalence · order_basics, add_inverse — 加 1 與加 −1 互為反運算，對任何實數都可做，所以雙向成立（N9）。
- S10 · premise_audit · square_nonneg, L_shift, subset_def — 這是 ⊆ 方向；⊇ 方向（每個 y≥1 都被取到）另需 S11、S12。
- S09 · premise_audit · function_def, S04, injective_surjective_def — 結論依賴陪域是函數資料的一部分；只看輸出表無法判定陪域（MKO 第二段）。
- S08 · premise_audit · function_def, G1 — 只需一個沒有輸出的輸入就足以否定總函數。
- S07 · premise_audit · S02, function_def — 只需一個輸出落在宣告陪域外就足以否定；N5 核對 5>4。
- S06 · premise_audit · S04, set_extensionality, set_operations_def — 證明不相等只需一個在 B 中而不在 f[A] 中的元素；這裡是 0。
- S05.1 · premise_audit · image_preimage_def, function_def, subset_def, exists_elim — 只用到「輸出必須在陪域中」這一條；若允許輸出落在 B 外（如 S07），結論就失效。
- S05 · premise_audit · L_range_sub, S03 — 引理需要 f 真的是 A→B 的總函數（S03）。只宣稱包含，不宣稱相等。
- S04 · inverse_equivalence · set_extensionality, image_preimage_def — 兩邊有相同的元素，依外延原則是同一個集合，雙向成立。
- S03 · premise_audit · S02, function_def — 三個條件都必須逐輸入核對；S07、S08 是各缺一個條件的非實例。
- S02 · premise_audit · G1, numeric_evaluation — 四個值可獨立重算（N1 到 N4）；A 的每個元素都算到，沒有遺漏。
- S01 · premise_audit · G3, mko_dcr_def — 此步只寫出定義，不推出新事實。





## 錯誤控制與反例

陪域不是值域MKO 指出的第一個誤解是把陪域當成實際值域。f 的陪域 B 有 6 個元素，值域只有 {1,2,5}；h 的陪域是 ℝ，值域卻是 [1,∞)。陪域是宣告「輸出必須落在哪裡」，值域要從實際輸出算出來，兩者只有在滿射時才相等。

先確認是總函數，再談值域MKO 指出的第二個誤解是以有未定義輸入的表格計算宣稱的總函數的值域。漏掉輸入 2 的表格會給出 {1,2}，少了 5；輸出 5 落在宣告的 {0,1,2,3,4} 之外，則那份宣告根本不是函數。先逐輸入核對三個條件（S03），值域才有意義。

同樣的對應、不同的陪域是不同的函數資料f:A→B 與 f_C:A→{1,2,5} 對每個輸入給出相同的值，值域也相同，但陪域不同，所以是不同的函數資料；前者不是滿射，後者是。只看輸出表無法得知陪域（MKO 第二段）。


- f:A→B 的值域是 B={0,1,2,3,4,5} → reject — f[A]={1,2,5}；0、3、4 不是任何輸入的輸出。
- h:ℝ→ℝ、h(x)=x²+1 的值域是 ℝ → reject — x²+1≥1，所以 0 不在值域中；值域是 [1,∞)。
- 只列 −1、0、1 的表格是 A 上的總函數，值域為 {1,2} → reject — 2∈A 沒有輸出；真正的 f[A] 還含 5。
- 規則 x²+1 可宣告為 A→{0,1,2,3,4} 的總函數 → reject — f(2)=5 不在 {0,1,2,3,4} 中。
- 值域 {2,1,2,5} 有四個元素 → reject — 重複輸出只算一次；f[A]={1,2,5} 有 3 個元素。





## 結論與限制

f:A→B（A={−1,0,1,2}、B={0,1,2,3,4,5}、f(x)=x²+1）是總函數，值域 f[A]={1,2,5}⊆B，但 0、3、4 不在值域中，所以 f[A]≠B。輸出 5 落在 {0,1,2,3,4} 外、或漏掉輸入 2 的資料，都不是本條目的總函數。h:ℝ→ℝ、h(x)=x²+1 的值域是 [1,∞)，不等於陪域 ℝ。


- N6 是 x 從 −20 到 20 的整數點上的有限核對，只支持這些點；一般結論 x²+1≥1 來自 S10 的論證。





## 驗證及來源綁定

11 個本稿宣告算術檢查；只支持所列算式。


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 8bda61e820ecd87d075b98c8407ebfb669c073e33b1825b598e48d1e4176933c
- original source SHA-256: 8bda61e820ecd87d075b98c8407ebfb669c073e33b1825b598e48d1e4176933c
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-domain-codomain-range-01.json)