Menger–Nöbeling の埋め込み定理
を空でないコンパクト距離空間、 を整数とし、 とします。このとき から への埋め込み（同相写像として像への）が存在します。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 27 件、定義なども含めて 34 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 10 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
C(K) の完備性✓補題 2.1・Arzelà–Ascoli と Stone–Weierstrass
実数の完備性（コーシーの収束判定法）✓定理 7.3・実数の完備性とコーシー列
コーシー列の基本性質✓命題 7.2・実数の完備性とコーシー列
- 数列の収束・有界性・単調性定義 2.2・実数の完備性とコーシー列
- コーシー列定義 7.1・実数の完備性とコーシー列
ボルツァーノ・ワイエルシュトラスの定理✓定理 6.3・実数の完備性とコーシー列
- 単調部分列の補題✓補題 6.2・実数の完備性とコーシー列
- 完備性の公理（単調収束の原理）公理 3.1・実数の完備性とコーシー列
- コーシー列定義 7.1・実数の完備性とコーシー列
- 部分列定義 6.1・実数の完備性とコーシー列
Tychonoff の定理✓定理 6.2・積位相・商位相と Tychonoff の定理
コンパクト性の超フィルターによる特徴づけ✓定理 5.9・積位相・商位相と Tychonoff の定理
- 超フィルターの特徴づけ✓補題 5.7・積位相・商位相と Tychonoff の定理
超フィルターの像は超フィルター✓補題 6.1・積位相・商位相と Tychonoff の定理
- 超フィルターの特徴づけ✓補題 5.7・積位相・商位相と Tychonoff の定理
- 選択公理公理 3.1・選択公理と Zorn の補題
コンパクト空間の閉部分集合はコンパクト✓定理 4.1・コンパクト性
- 部分空間のコンパクト性の判定✓補題 3.3・コンパクト性
コンパクト集合の連続像はコンパクト✓定理 6.1・コンパクト性
- 部分空間のコンパクト性の判定✓補題 3.3・コンパクト性
ハイネ・ボレルの定理✓定理 5.2・コンパクト性
閉直方体はコンパクト✓補題 5.1・コンパクト性
- 部分空間のコンパクト性の判定✓補題 3.3・コンパクト性
- コンパクト空間の閉部分集合はコンパクト✓定理 4.1・コンパクト性（上で展開済み）
- ハウスドルフ空間定義 2.1・コンパクト性
ハウスドルフ空間ではコンパクト集合と外部の点が分離できる✓定理 4.2・コンパクト性
- ハウスドルフ空間定義 2.1・コンパクト性
- 部分空間のコンパクト性の判定✓補題 3.3・コンパクト性
- 部分空間のコンパクト性の判定✓補題 3.3・コンパクト性
コンパクト距離空間上の連続関数は一様連続✓補題 2.2・Arzelà–Ascoli と Stone–Weierstrass
距離空間のコンパクト性の同値条件✓定理 4.3・距離空間
- ルベーグ数の補題✓補題 4.2・距離空間
- ルベーグ数の補題✓補題 4.2・距離空間
コンパクト距離空間の被覆次元の判定✓補題 2.2・次元論の入口
- コンパクト空間定義 3.2・コンパクト性
- 距離空間のコンパクト性の同値条件✓定理 4.3・距離空間（上で展開済み）
- ルベーグ数の補題✓補題 4.2・距離空間
- 有限個の超平面では覆えない✓補題 6.2・次元論の入口
Baire のカテゴリー定理✓定理 5.1・距離空間
- 閉集合と点列、完備部分空間✓命題 2.3・距離空間
コンパクトからハウスドルフへの連続全単射は同相✓系 6.5・コンパクト性
- コンパクト空間の閉部分集合はコンパクト✓定理 4.1・コンパクト性（上で展開済み）
- コンパクト集合の連続像はコンパクト✓定理 6.1・コンパクト性（上で展開済み）
- ハウスドルフ空間ではコンパクト集合と外部の点が分離できる✓定理 4.2・コンパクト性（上で展開済み）
これを使っている定理
証明で明示的に参照している定理は、まだありません。