位相空間¶

位相空間構造は TopologicalSpace X です．開集合は IsOpen U，閉集合は IsClosed C と書きます． interior，closure，frontier なども Set X に対する操作です．

Mathlib では，位相空間構造の中に開集合を表す述語が入っています． IsOpen はその述語を取り出したものです．一方，IsClosed C は独立した原始概念ではなく，補集合 Cᶜ が開集合であることとして定義されています．

Mathlib/Topology/Defs/Basic.lean

class TopologicalSpace (X : Type u) where
  protected IsOpen : Set X → Prop
  protected isOpen_univ : IsOpen univ
  protected isOpen_inter : ∀ s t, IsOpen s → IsOpen t → IsOpen (s ∩ t)
  protected isOpen_sUnion : ∀ s, (∀ t ∈ s, IsOpen t) → IsOpen (⋃₀ s)

def IsOpen : Set X → Prop := TopologicalSpace.IsOpen

class IsClosed (s : Set X) : Prop where
  isOpen_compl : IsOpen sᶜ

したがって，閉集合に関する主張は，補集合を取ると開集合に関する主張として読めます．

#check TopologicalSpace
#check IsOpen
#check IsClosed
#check interior
#check closure
#check frontier

section TopologicalSpaces

variable {X : Type*} [TopologicalSpace X]
variable {U V C D Y Z : Set X}

example (hU : IsOpen U) (hV : IsOpen V) : IsOpen (U ∩ V) := by
  exact hU.inter hV

example (hC : IsClosed C) (hD : IsClosed D) : IsClosed (C ∪ D) := by
  exact hC.union hD

example : IsOpen Cᶜ ↔ IsClosed C := by
  exact isOpen_compl_iff

example : interior Y = Y ↔ IsOpen Y := by
  exact interior_eq_iff_isOpen

example (hYZ : Y ⊆ Z) : interior Y ⊆ interior Z := by
  exact interior_mono hYZ

example : closure Y = Y ↔ IsClosed Y := by
  exact closure_eq_iff_isClosed

example (hYZ : Y ⊆ Z) : closure Y ⊆ closure Z := by
  exact closure_mono hYZ

end TopologicalSpaces

集合の等式や包含と同じように，位相的な操作も Set の補題と組み合わせて使います．たとえば，closure_mono は集合の包含から閉包の包含を得る補題です．

演習問題¶

closure_mono を使って，s ⊆ t なら closure s ⊆ closure t を示してください．

example {X : Type*} [TopologicalSpace X] {s t : Set X} (hst : s ⊆ t) :
    closure s ⊆ closure t := by
  -- ヒント: `exact closure_mono hst`
  -- 解答例: exact closure_mono hst
  sorry

interior s ⊆ s と s ⊆ closure s をそれぞれ確認してください．

-- 解答例: `interior_subset` が `interior s ⊆ s`，
-- `subset_closure` が `s ⊆ closure s` を述べます．
#check interior_subset
#check subset_closure