# 函數合成

合成 g∘f 先求 f 的輸出，再把它送入 g；合成前須確認中間值可作為 g 的輸入。

mko-composition · definition · v0.10.0



## 數學敘述

若 f:A→B、g:B→C 為總函數，則 g∘f:A→C 由 (g∘f)(x)=g(f(x)) 定義。對不同定義域的表達式，合成允許的輸入為 {x∈dom(f):f(x)∈dom(g)}。





## 代表公式（精確 TeX）

g(f(x))





## 成立條件


- 函数及其定義域、陪域已明示。
- 完整總函數合成的中間型別相容；受限合成只在明示允許集合上求值。





## 符號作用域


- g — 外層函數
- f — 內層函數
- x — 輸入





## 直觀、定義與常見誤解

g(f(x)) 必須先完成 f(x)，再求 g；合成符號的書寫順序與實際求值順序相反。

若中間值不屬於 g 的定義域，就不能在該輸入求合成。有限表格可明確列出允許的合成定義域。

函數合成一般不交換，也不是函數值的乘法；任意改寫為 f(g(x)) 或 f(x)g(x) 都需要額外條件。

把 g∘f 誤讀成先 g 後 f，或略過中間值的定義域檢查。





## 已採用的推導導讀

[函數合成：受限合成的允許輸入、求值順序與不交換](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-composition-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [定義域、陪域與值域](https://ocme.evemisslab.com/zh-Hant/mko/mko-domain-codomain-range/) — 合成需要檢查第一輸出與第二輸入的集合邊界。





## 驗證界線

有限表格與指定線性表达式可精確重算；不構成全部函數等式或定義域法則的形式證明。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

綁定 Function.comp 及集合限制上的合成定義域；另處理型別轉換條件。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/composition.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-composition/index.md)