長めの例: 連続関数の零点集合は閉集合¶

位相の典型的な主張として，連続関数 f : X → ℝ の零点集合

{x | f x = 0}

は閉集合です．紙の証明では「{0} は ℝ の閉集合で，零点集合はその逆像である」と説明します． Lean でも同じ構造で証明します．

def zeroSet {X : Type*} (f : X → ℝ) : Set X :=
  {x | f x = 0}

section ZeroSet

variable {X : Type*} [TopologicalSpace X]
variable {f : X → ℝ}

example (hf : Continuous f) : IsClosed (zeroSet f) := by
  simpa [zeroSet] using isClosed_singleton.preimage hf

example (hf : Continuous f) (c : ℝ) : IsClosed {x : X | f x = c} := by
  simpa using isClosed_eq hf continuous_const

end ZeroSet

2 つ目の例は，level set {x | f x = c} が閉集合であることを示しています．証明では {x | f x = c} を {x | f x - c = 0} と見て，連続関数 x ↦ f x - c の零点集合として扱っています．

simpa は，このような表現の差を整理するためによく使います．

演習問題¶

zeroSet を使わずに {x | f x = 0} が閉集合であることを直接証明してください．

example {X : Type*} [TopologicalSpace X] {f : X → ℝ} (hf : Continuous f) :
    IsClosed {x : X | f x = 0} := by
  -- `isClosed_eq hf continuous_const` を使う．
  -- 解答例: simpa using isClosed_eq hf continuous_const
  sorry