| 英語 | 日本語 |
|---|---|
| absorption laws | 吸収則 |
| almost everywhere | ほとんどいたるところ |
| analysis | 解析学 |
| arguments | 引数 |
| arithmetic | 算術 |
| associativity | 結合性 |
| axiom of choice | 選択公理 |
| ball | 球体 |
| bijection | 全単射 |
| bi-implication | 双方向の含意 |
| bipartite graph | 2部グラフ |
| bundled maps | 束縛写像 |
| canonical topology | 正準位相 |
| cardinality | 濃度 |
| carrier set | 台集合 |
| carrier type | 台の型 |
| cauchy sequence | コーシー列 |
| closed sets | 閉集合 |
| closure | 閉包 |
| closure property | 閉性 |
| change-of-variables | 変数変換 |
| chapter | 章 |
| cluster point | 集積点 |
| codomain | 終域 |
| coercion | 型の強制 |
| complete | 完備 |
| complete lattice | 完備束 |
| conjunction | 連言 |
| context | コンテキスト |
| continuum hypothesis | 連続体仮説 |
| contravariant | 反変 |
| convergence | 収束 |
| coprime | 互いに素 |
| curly brackets | 波括弧 |
| cycle | 巡回置換 |
| dense | 稠密 |
| dependent type theory | 依存型理論 |
| definitional equality | 定義上の等しさ |
| derivative function | 導関数 |
| derivative of ~ | ~での微分係数 |
| descend | （自然な全単射などへ）誘導される |
| direct image | 順像 |
| disjunction | 選言 |
| distributive lattice | 分配束 |
| divisibility relation | 整除関係 |
| domain | 始域 |
| dominated convergence theorem | 優収束定理 |
| endomorphisms | 自己準同型 |
| entourage | 近縁 |
| eta-reduction | η簡約 |
| Euclidean algorithm | ユークリッドの互助法 |
| Euclidean domain | ユークリッド整域 |
| excluded middle | 排中律 |
| exercises | 演習 |
| ex falso | 爆発律 |
| existential quantifier | 存在量化子 |
| extensionality | 外延性 |
| factorial | 階乗 |
| filter | フィルタ |
| filter basis | フィルタ基底 |
| first countability | 第一可算 |
| free group | 自由群 |
| functoriality | 関手性 |
| full subgroup | 完全部分群 |
| Galois connection | ガロア接続 |
| gaussian integer | ガウス整数 |
| greatest common divisor | 最大公約数 |
| greatest lower bound | 最大下界 |
| group action | 群作用 |
| group presentation | 群の表示 |
| higher-order unification | 高階ユニフィケーション |
| identity | 恒等式, 等式 |
| if-and-only-if statement | 同値性を主張する文 |
| iff | 必要十分条件 |
| image | 像 |
| inclusion | 包含 |
| indeterminate | 不定元 |
| induction | 帰納法 |
| infimum | 下限 |
| integral domain | 整域 |
| internal direct sum | 内部直和 |
| intersection | 共通部分 |
| irrational | 無理数 |
| irreducible | 既約元 |
| join | 結び |
| lattice | 束 |
| lowest term | 既約分数 |
| least common multiple | 最小公倍数 |
| least upper bound | 最小上界 |
| library | Mathlib（Mathlibを指していることが明白である場合） |
| logical connective | 論理結合子 |
| mass | 体積量 |
| measure theory | 測度論 |
| meet | 交わり |
| membership | 帰属 |
| metric space | 距離空間 |
| metric space topology | 距離空間位相 |
| module | 加群 |
| monotone | 単調 |
| morphism | 射 |
| multilinear maps | 多重線形写像 |
| natural domain | 自然な定義域 |
| neighborhood basic | 基本近傍 |
| norm | ノルム |
| normed space | ノルム空間 |
| normed vector space | ノルム線形空間 |
| number systems | 数体系 |
| number theory | 数論 |
| open interval | 開区間 |
| open sets | 開集合 |
| operator | 演算子（中置記法の定義等なにかしら特殊な記法が用意されている場合）、関数（それ以外） |
| operator norm | 作用素ノルム |
| orbit | 軌道（群論） |
| ordered ring | 順序環 |
| preimage | 逆像 |
| partial order | 半順序 |
| partially bundled structure | 部分的に束ねられた構造体 |
| permutations | 置換 |
| principal filter | 主フィルタ |
| proof term | 証明項 |
| proof by contradiction | 背理法 |
| pullback | 引き戻し |
| pushforward | 押し出し |
| quadratic integers | 二次体の整数 |
| quotient | 商 |
| r-simplex | r単体 |
| real analysis | 実解析 |
| reflexivity | 反射性 |
| recursion | 再帰 |
| root | 根 |
| section | 節 |
| sequence | 数列 |
| segment | 線分 |
| set-builder notation | 内包表記 |
| simplify | 単純化 |
| simplifier | simp |
| singleton | 単集合 |
| span | 空間を張る |
| stabilizer | 固定部分群（群論） |
| statement | 命題 |
| strictly differentiable | 狭義微分可能 |
| strict partial order | 狭義半順序 |
| strong induction | 強帰納法 |
| sub-object | 部分対象 |
| subset | 部分集合 |
| support | 台 |
| supremum | 上限 |
| surjective | 全射 |
| symmetric group | 対称群 |
| tend to ~ | ~に収束する |
| topological group | 位相群 |
| topological space | 位相空間 |
| total order | 全順序 |
| transitivity | 推移性 |
| translation | 移動作用（群論） |
| triangle inequality | 三角不等式 |
| type ascription | 型アスクリプション |
| uncountable | 不可算 |
| Uniform Boundedness Principle | 一様有界性原理 |
| uniformly continuous | 一様連続 |
| uniform space | 一様空間 |
| union | 合併, 非交和 |
| univariate polynomial | 一変数多項式 |
| universal property | 普遍性 |
| universal quantifier | 全称量化子 |
| up to definitional equality | 定義上の等しさを除いて（ベーシック圏論にてunique up to isomorphismを「同型を除いて一意」と訳されていることに合わせた） |
| well-founded | 整礎関係 |
| well-formed | 合法 |
| well-formed formula | 論理式 |
| zero divisor | 零因子 |