拓撲連續映射

數學敘述

給定拓撲空間 (X,τX)、(Y,τY) 與總映射 f:X→Y，f 連續當且僅當對每個 V∈τY，逆像 f⁻¹[V]∈τX。這是逆像條件，不要求開集的像為開。

代表公式（精確 TeX）

f:X\to Y

成立條件

• 來源、目標底集合與兩個拓撲均固定。
• f 是完整總表；逆像按目標子集合收集所有映入其中的來源元素。

符號作用域

• f — 拓撲空間間的總映射
• X — 來源空間
• Y — 目標空間

直觀、定義與常見誤解

有限拓撲中可以逐一列出目標所有開集並重算逆像，因此完整判定給定表是否連續。

連續映射的合成仍連續；有限模型可重算兩段映射與每個開集逆像，不能只抽樣單點。

開映射要求開集的像為開，與連續性不同。映射可能連續但不是開映射，也可能是開映射但不連續。

把開集的像為開當成連續定義，或只抽查一個開集。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 拓撲空間 — 來源與目標各有開集族。
• 開集與閉集 — 連續性核對目標開集及來源逆像。
• 函數映射 — 逆像由完整總映射定義。

驗證界線

完整有限拓撲可精確判定；不宣稱既有實函數連續條目的所有語義已自動等價。

not_formalized

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

下一個義務

綁定 Mathlib Continuous 的 open-preimage 定義，另建立實函數、子空間與孤立點語義橋。

同源結構化資料

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