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

目標與範圍

(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。

逐步主鏈

f:A\to B

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

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

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

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

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

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

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

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

f[A]\subseteq B

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\}

\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'

\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

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

x\in\mathbb{R}

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

y\in[1,\infty)

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

t^2=y-1

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

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

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

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

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

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

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

局部子步與引理

y\in f[A]

y\in B

u\geq 0

u+1\geq 1

逐步反向審查

• 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、反控制與修訂記錄）