普遍被覆の存在

定理 7.1（「基本群と被覆空間」§7）・ ✓公理まで証明済み

道連結・局所道連結・半局所単連結な空間 $X$ は普遍被覆を持つ。

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 15 件、定義なども含めて 16 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

基点の取り替え✓命題 2.4・基本群と被覆空間
- 道の積の群的性質✓命題 2.2・基本群と被覆空間
道の積の群的性質✓命題 2.2・基本群と被覆空間
ホモトピーの持ち上げ✓定理 3.6・基本群と被覆空間
- 持ち上げの一意性✓補題 3.5・基本群と被覆空間
  - 連結性の特徴づけ✓命題 3.1・連結性
- Lebesgue 数✓補題 3.4・基本群と被覆空間
  - 最大値・最小値の定理✓系 6.2・コンパクト性
    コンパクト集合の連続像はコンパクト✓定理 6.1・コンパクト性この先をたどる →
    ハイネ・ボレルの定理✓定理 5.2・コンパクト性この先をたどる →
被覆写像が誘導する準同型は単射✓命題 3.8・基本群と被覆空間
- 系 3.7✓基本群と被覆空間
  - ホモトピーの持ち上げ✓定理 3.6・基本群と被覆空間（上で展開済み）

証明で明示的に参照している定理は、まだありません。