structure Filter (α : Type*) where sets : Set (Set α) -- 集合的集合 univ_sets : univ ∈ sets -- 全集在其中 sets_of_superset {U V} : U ∈ sets → U ⊆ V → V ∈ sets -- 向上封闭 inter_sets {U V} : U ∈ sets → V ∈ sets → U ∩ V ∈ sets -- 对交封闭
U ∈ F 的含义
U ∈ F 即 U ∈ F.sets。可以把滤子想象成一个”充分大集合”的族。
11.1.2 常用滤子
open Filter-- 𝓟 = \MCP（主滤子），包含 s 的所有超集-- Ioo = open interval open，即开区间 (a, b)def principal {α : Type*} (s : Set α) : Filter α where sets := { t | s ⊆ t } ...-- 自然数的余尾滤子example : Filter ℕ := { sets := { s | ∃ a, ∀ b, a ≤ b → b ∈ s } ... }-- 邻域滤子#check (𝓝 x₀ : Filter ℝ) -- x₀ 的邻域滤子-- 积滤子example (x₀ y₀ : ℝ) : 𝓝 (x₀, y₀) = 𝓝 x₀ ×ˢ 𝓝 y₀ := nhds_prod_eq
11.1.3 滤子的推前与拉回
-- map = 推前（像的滤子）#check Filter.map f F -- f_* F-- comap = 拉回（原像的滤子）#check Filter.comap f G -- f^* G-- Galois 连接#check Filter.map_le_iff_le_comap : map f F ≤ G ↔ F ≤ comap f G-- comap 的逆变复合#check comap_comap : comap m (comap n F) = comap (n ∘ m) F
直观理解
map u atTop ≤ 𝓝 x₀ = “u 把充分大的自然数映射到 x₀ 的充分近邻域中”
11.1.4 Tendsto：统一的极限
-- 定义1（用集合成员）def Tendsto₁ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) := ∀ V ∈ G, f ⁻¹' V ∈ F-- 定义2（用滤子序，更代数化）def Tendsto₂ {X Y : Type*} (f : X → Y) (F : Filter X) (G : Filter Y) := map f F ≤ G-- 两者等价example : Tendsto₂ f F G ↔ Tendsto₁ f F G := Iff.rfl
Tendsto 的威力
Tendsto u atTop (𝓝 x) = 序列 u 收敛到 xTendsto f (𝓝 x₀) (𝓝 y₀) = lim_{x→x₀} f(x) = y₀Tendsto f (𝓝[Ioi x₀] x₀) (𝓝 y₀) = 右极限
全部统一为同一种类型！
极限的复合（一次证明，覆盖所有 512 种情况）：
#check @Filter.map_mono -- map 保序#check @Filter.map_map -- map 与复合相容example {f : X → Y} {g : Y → Z} (hf : Tendsto f F G) (hg : Tendsto g G H) : Tendsto (g ∘ f) F H := by rw [Tendsto₂] at hf hg ⊢ calc map (g ∘ f) F = map g (map f F) := by rw [map_map] _ ≤ map g G := by gcongr _ ≤ H := hg
11.1.5 滤子基与收敛的等价刻画
-- Ioo a b = {x | a < x ∧ x < b} = 开区间 (a, b)-- ℝ 上邻域的基：开区间 (x₀-ε, x₀+ε)example (x₀ : ℝ) : HasBasis (𝓝 x₀) (fun ε : ℝ ↦ 0 < ε) fun ε ↦ Ioo (x₀ - ε) (x₀ + ε) := nhds_basis_Ioo_pos x₀-- 用基重新表述收敛example (u : ℕ → ℝ) (x₀ : ℝ) : Tendsto u atTop (𝓝 x₀) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, u n ∈ Ioo (x₀ - ε) (x₀ + ε) := by have : atTop.HasBasis (fun _ : ℕ ↦ True) Ici := atTop_basis rw [this.tendsto_iff (nhds_basis_Ioo_pos x₀)] simp
11.1.6 Eventually 与 Frequently
-- ∀ᶠ n in atTop, P n = "对充分大的 n，P n 成立"example (P Q : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n) : ∀ᶠ n in atTop, P n ∧ Q n := hP.and hQ-- 两个序列最终相等 ⇒ 收敛性相同example (u v : ℕ → ℝ) (h : ∀ᶠ n in atTop, u n = v n) (x₀ : ℝ) : Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) := tendsto_congr' h-- 记号：u =ᶠ[atTop] vexample (u v : ℕ → ℝ) (h : u =ᶠ[atTop] v) (x₀ : ℝ) : Tendsto u atTop (𝓝 x₀) ↔ Tendsto v atTop (𝓝 x₀) := tendsto_congr' h
filter_upwards tactic
组合多个 Eventually 假设：
example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n) (hR : ∀ᶠ n in atTop, P n ∧ Q n → R n) : ∀ᶠ n in atTop, R n := by filter_upwards [hP, hQ, hR] with n h h' h'' exact h'' ⟨h, h'⟩
11.1.7 ClusterPt 与闭包
-- ClusterPt x F = "x 的每个邻域与 F 的每个集合相交"example {x : X} {F : Filter X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) := Iff.rfl-- 收敛 + 序列在集合中 ⇒ 极限在闭包中example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x)) (huM : ∀ᶠ n in atTop, u n ∈ M) : x ∈ closure M := mem_closure_of_tendsto hux huM
variable {X : Type*} [MetricSpace X] (a b c : X)#check (dist a b : ℝ)#check (dist_nonneg : 0 ≤ dist a b)#check (dist_eq_zero : dist a b = 0 ↔ a = b)#check (dist_comm a b : dist a b = dist b a)#check (dist_triangle a b c : dist a c ≤ dist a b + dist b c)
11.2.2 收敛与连续性
-- 序列收敛（等价于 ε-N 定义）example {u : ℕ → X} {a : X} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := Metric.tendsto_atTop-- 连续性的 ε-δ 刻画example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} : Continuous f ↔ ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := Metric.continuous_iff-- 在一点连续example {f : X → Y} (a : X) : ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x}, dist x a < δ → dist (f x) (f a) < ε := Metric.continuousAt_iff
11.2.3 连续性证明技巧
example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) : Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by continuity -- tactic 自动证明
手动证明的多种方式：
-- 方式1：显式复合example (hf : Continuous f) : Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := continuous_dist.comp ((hf.comp continuous_fst).prodMk (hf.comp continuous_snd))-- 方式2：用 Continuous.dist（对 elaborator 更友好）example (hf : Continuous f) : Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := by apply Continuous.dist · exact hf.comp continuous_fst · exact hf.comp continuous_snd-- 方式3：用 Continuous.fst' / snd'example (hf : Continuous f) : Continuous fun p : X × X ↦ dist (f p.1) (f p.2) := hf.fst'.dist hf.snd'
composition elaboration 问题
Lean 的 elaborator 不擅长识别 fun p ↦ dist (f p.1) (f p.2) 是 dist ∘ (fun p ↦ (f p.1, f p.2)) 的复合。
用 Continuous.dist 或 continuity tactic 避免此问题。
11.2.4 球、开集与闭集
variable (r : ℝ)-- 开球与闭球example : Metric.ball a r = { b | dist b a < r } := rflexample : Metric.closedBall a r = { b | dist b a ≤ r } := rfl-- 开集的球刻画example (s : Set X) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s := Metric.isOpen_iff-- 闭集 = 补集开example {s : Set X} : IsClosed s ↔ IsOpen (sᶜ) := isOpen_compl_iff.symm-- 闭集对极限封闭example {s : Set X} (hs : IsClosed s) {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) (hus : ∀ n, u n ∈ s) : a ∈ s := hs.mem_of_tendsto hu (Eventually.of_forall hus)-- 闭包example {s : Set X} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, a ∈ Metric.ball b ε := Metric.mem_closure_iff
邻域的基
example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s := Metric.nhds_basis_ball.mem_iff
11.2.5 紧致性
-- [0,1] 紧致example : IsCompact (Set.Icc 0 1 : Set ℝ) := isCompact_Icc-- 紧致集上的序列有收敛子列example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) : ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) := hs.tendsto_subseq hu-- 极值定理example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f s) : ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y := hs.exists_isMinOn hs' hfs-- 紧致 ⇒ 闭example {s : Set X} (hs : IsCompact s) : IsClosed s := hs.isClosed-- 全局紧致example {X : Type*} [MetricSpace X] [CompactSpace X] : IsCompact (univ : Set X) := isCompact_univ
11.2.6 一致连续性与完备性
-- 一致连续example {X Y : Type*} [MetricSpace X] [MetricSpace Y] {f : X → Y} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := Metric.uniformContinuous_iff-- 紧致 ⇒ 一致连续example {X : Type*} [MetricSpace X] [CompactSpace X] {Y : Type*} [MetricSpace Y] {f : X → Y} (hf : Continuous f) : UniformContinuous f := by sorry -- 练习-- Cauchy 序列example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := Metric.cauchySeq_iff-- 完备空间：Cauchy 序列收敛example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete hu
11.2.7 Baire 定理
example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd : ∀ n, Dense (f n)) : Dense (⋂ n, f n) := by sorry -- 经典证明：构造 Cauchy 序列，用完备性得到极限点
11.3 Topological Spaces
核心洞见
拓扑空间只保留连续性的信息。它比度量空间更函子化：
任意映射可推前/拉回拓扑
任意积/余积/商都有拓扑
TopologicalSpace X 是完备格
11.3.1 开集公理
variable {X : Type*} [TopologicalSpace X]example : IsOpen (univ : Set X) := isOpen_univexample : IsOpen (∅ : Set X) := isOpen_emptyexample {ι : Type*} {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) : IsOpen (⋃ i, s i) := isOpen_iUnion hsexample {ι : Type*} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) : IsOpen (⋂ i, s i) := isOpen_iInter_of_finite hs
11.3.2 两种等价观点
观点1：开集
example {f : X → Y} : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) := continuous_def
观点2：邻域滤子（Mathlib 更常用）
example {f : X → Y} {x : X} : ContinuousAt f x ↔ map f (𝓝 x) ≤ 𝓝 (f x) := Iff.rflexample {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ U ∈ 𝓝 (f x), ∀ᶠ x in 𝓝 x, f x ∈ U := Iff.rfl-- 邻域 = 包含开集的集合example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := mem_nhds_iff
为什么 Mathlib 偏好邻域观点？
因为连续性在一点处的定义更自然：f 把”接近 x”的点映射到”接近 f(x)“的点。
11.3.3 从邻域函数构造拓扑
邻域函数 n : X → Filter X 必须满足两个条件：
-- 1. 每个点在自己的邻域中example (x : X) : pure x ≤ 𝓝 x := pure_le_nhds x-- 2. "接近"具有传递性example {P : X → Prop} {x : X} (h : ∀ᶠ y in 𝓝 x, P y) : ∀ᶠ y in 𝓝 x, ∀ᶠ z in 𝓝 y, P z := eventually_eventually_nhds.mpr h
11.3.4 拓扑的函子性
推前（coinduced）与拉回（induced）：
example (f : X → Y) : TopologicalSpace X → TopologicalSpace Y := TopologicalSpace.coinduced f -- f_* T_Xexample (f : X → Y) : TopologicalSpace Y → TopologicalSpace X := TopologicalSpace.induced f -- f^* T_Y-- Galois 连接example (f : X → Y) (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) : TopologicalSpace.coinduced f T_X ≤ T_Y ↔ T_X ≤ TopologicalSpace.induced f T_Y := coinduced_le_iff_le_induced
推前的泛性质
g : Y → Z 对 f_* T_X 连续 ⇔ g ∘ f 对 T_X 连续。
这直接给出商拓扑的存在性。
完备格结构：
-- T ≤ T' 当且仅当 T' 的开集都是 T 的开集--（注意：拓扑越"细"，开集越多，但在序中越小！）example {T T' : TopologicalSpace X} : T ≤ T' ↔ ∀ s, T'.IsOpen s → T.IsOpen s := Iff.rfl-- 连续性 = 推前 ≤ 目标拓扑example (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) (f : X → Y) : Continuous f ↔ TopologicalSpace.coinduced f T_X ≤ T_Y := continuous_iff_coinduced_le
积拓扑的存在性（抽象推理）：
example (ι : Type*) (X : ι → Type*) (T_X : ∀ i, TopologicalSpace (X i)) : (Pi.topologicalSpace : TopologicalSpace (∀ i, X i)) = ⨅ i, TopologicalSpace.induced (fun x ↦ x i) (T_X i) := rfl
积拓扑 = 最粗的使所有投影连续
f : Z → Π i, X i 连续 ⇔ 每个分量 fun z ↦ f z i 连续。
度量空间不满足这个性质（不可数积没有度量）。
11.3.5 分离公理
-- T2 = Hausdorff：极限唯一example [TopologicalSpace X] [T2Space X] {u : ℕ → X} {a b : X} (ha : Tendsto u atTop (𝓝 a)) (hb : Tendsto u atTop (𝓝 b)) : a = b := tendsto_nhds_unique ha hb-- T3 = Regular + T1：每个点有闭邻域基example [TopologicalSpace X] [RegularSpace X] (a : X) : (𝓝 a).HasBasis (fun s : Set X ↦ s ∈ 𝓝 a ∧ IsClosed s) id := closed_nhds_basis a-- 每个点有开邻域基（总是成立）example [TopologicalSpace X] {x : X} : (𝓝 x).HasBasis (fun t : Set X ↦ t ∈ 𝓝 x ∧ IsOpen t) id := nhds_basis_opens' x
11.3.6 延拓定理
-- 延拓连续性定理（Bourbaki I.8.5）example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f) (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) (𝓝 x)) (𝓝 c)) : ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := by sorry
11.3.7 可数性
-- 第一可数：每个点有可数的邻域基-- 重要推论：闭包可用序列刻画example [TopologicalSpace X] [FirstCountableTopology X] {s : Set X} {a : X} : a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) := mem_closure_iff_seq_limit
11.3.8 紧致性（拓扑版本）
variable [TopologicalSpace X]-- 紧致 = 每个非平凡滤子有聚点example {s : Set X} : IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := Iff.rfl-- 紧致集的连续像紧致example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) : IsCompact (f '' s) := by sorry -- 用 filter 证明-- 有限覆盖性质example {ι : Type*} {s : Set X} (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i := hs.elim_finite_subcover U hUo hsU
本章核心概念总结
概念
类型/记号
含义
滤子
Filter α
”充分大”集合的族
主滤子
𝓟 s
包含 s 的超集
邻域滤子
𝓝 x
x 的邻域
余尾滤子
atTop
充分大的自然数
推前
map f F
f_* F
拉回
comap f G
f^* G
极限
Tendsto f F G
map f F ≤ G
积滤子
F ×ˢ G
comap fst F ⊓ comap snd G
Eventually
∀ᶠ x in F, P x
”对 F-充分大的 x，P x”
Frequently
∃ᶠ x in F, P x
”对任意 F-大的集合，存在 x 使 P x”
度量空间
[MetricSpace X]
dist + 公理
开球
Metric.ball x ε
`{y
闭球
Metric.closedBall x ε
`{y
紧致
IsCompact s
滤子版本或有限覆盖
Cauchy 序列
CauchySeq u
彼此最终接近
完备
[CompleteSpace X]
Cauchy ⇒ 收敛
拓扑空间
[TopologicalSpace X]
IsOpen + 公理
推前拓扑
coinduced f
商拓扑
拉回拓扑
induced f
子空间拓扑
T2
[T2Space X]
Hausdorff，极限唯一
T3
[T3Space X]
Regular + T1
第一可数
[FirstCountableTopology X]
可数邻域基
关键学习策略
1. 极限证明模板
example {u : ℕ → ℝ} {x : ℝ} : Tendsto u atTop (𝓝 x) := by -- 方式1：用 ε-N 定义 rw [Metric.tendsto_atTop] intro ε ε_pos use ... sorry -- 方式2：用 filter 代数 rw [Tendsto] calc map u atTop ≤ ... := ... _ ≤ 𝓝 x := ...
2. 连续性证明模板
example {f : X → Y} : Continuous f := by -- 方式1：tactic continuity -- 方式2：开集原像 rw [continuous_def] intro s hs sorry -- 方式3：邻域 intro x rw [ContinuousAt, Tendsto] sorry
3. 拓扑构造模板
-- 商拓扑 = 推前example (f : X → Y) (T_X : TopologicalSpace X) : TopologicalSpace Y := TopologicalSpace.coinduced f T_X-- 子空间拓扑 = 拉回example (f : X → Y) (T_Y : TopologicalSpace Y) : TopologicalSpace X := TopologicalSpace.induced f T_Y-- 积拓扑 = inf of pullbacksexample (ι : Type*) (X : ι → Type*) (T : ∀ i, TopologicalSpace (X i)) : TopologicalSpace (∀ i, X i) := ⨅ i, TopologicalSpace.induced (fun x ↦ x i) (T i)