知識物件
去心實數論域的函數極限
在a附近排除a本身，以ε-δ控制函數值；點值不屬於去心極限條件。
OCME · 中英數學知識與推導
知識物件
從定義、條件與公式理解概念，再接續導讀、例題及證據。
知識物件
實函數的點值與連續
在全實數論域連續需要點值存在且與兩側極限一致；補點與原函數連續不可混用。
知識物件
實函數在一點的導數與差商
導數是非零步差商的兩側極限，不是任何一個有限步差商；絕對值尖點另保留不存在。
知識物件
多項式的和、乘積與合成微分
四條微分規則先保留可微前提；本輪只在有限整數係數多項式上精確計算。
知識物件
多項式原函數與常數選擇
原函數須在宣告區間導回f；本輪全R多項式以常數項固定0的有理係數原函數作可重播代表。
知識物件
有限區間上的多項式定積分
連續多項式的有向定積分與精確矩公式；有限左端黎曼和只是有限和，不冒充一般積分或微積分基本定理完成。
知識物件
微積分基本定理：連續前提與有向端點
在全實數連續前提下，累積定積分的導數還原被積函數；合法原函數給有向積分端點差。
知識物件
非空有限樹：連通、無環與唯一道路
非空有限簡單無向圖同時連通且無環才是樹；保留單點、度1葉及加一條新邊的唯一環。
知識物件
拓撲空間
拓撲空間由底集合與一族開集組成；開集族包含空集與全空間，並對任意聯集與有限交封閉。
知識物件
自然數整除
自然數 a 整除 b，表示存在自然數乘數 k 使 b=a·k；零的兩側行為必須分開。
知識物件
最大公因數與互質
gcd(a,b) 是同時整除 a、b 且被每個公因數整除的自然數；gcd=1 時稱互質。
知識物件
自然數質數
自然數質數是大於或等於 2，且正因數只有 1 與自身的自然數。
知識物件
自然數模同餘
固定正模數 n 時，a 與 b 模 n 同餘表示兩者除以 n 的餘數相同。
知識物件
決定問題
決定問題由輸入集合 X 與 yes-instance 子集合 Y⊆X 指定；decider 必須對每個合法輸入終止並回傳正確布林答案。
知識物件
證明助理中的形式陳述
形式陳述是在固定版本、imports、環境與 local context 中成功 elaboration，且型別為 Prop 的核心項。
知識物件
開集與閉集
在固定拓撲空間中，開集屬於拓撲；閉集的補集為開集，同一集合可以同時開且閉。
知識物件
鄰域
集合 N 是點 x 的鄰域，當且僅當 N 包含某個含 x 的開集；N 本身不必開。
知識物件
拓撲連續映射
拓撲映射連續，表示目標空間每個開集的逆像在來源空間仍是開集。
知識物件
抽象計算模型
有限狀態計算模型以狀態集、初始狀態集、步驟關係與停止狀態集描述可能執行。
知識物件
算法正確性
算法正確性分開部分正確性與終止性；總正確性需要兩者同時成立。
知識物件
漸近資源界
漸近上界、下界與緊界必須相對輸入大小、成本模型及全尾段量化定義。
知識物件
證明項
證明項是在固定形式環境與 context 中具有命題 P 型別，並可由 kernel 檢查的項 t。
知識物件
離散時間動力系統
離散時間動力系統以狀態空間、自映射與自然數時間描述逐步演化；有限軌道核對不自動給出一般穩定性。
知識物件
常微分方程
常微分方程關聯未知單變數函數及其有限階導數；候選函數的殘差核對不等於存在唯一性定理。