連続性の基本 API

前節では，Tendsto，𝓝 x，開集合の逆像による連続性を数式で読みました． ここからは，それらを Lean で使うときの名前を確認します．

関数 f : X → Y の大域的な連続性は Continuous f， 点 x での連続性は ContinuousAt f x， 集合 s 上での連続性は ContinuousOn f s です．

この節では定義をもう一度展開するのではなく，よく使う読み替えと操作だけを確認します．

• rfl: ContinuousAt f x を Tendsto f (𝓝 x) (𝓝 (f x)) と見る．
• continuousAt_def: 点での連続性を近傍の逆像条件として見る．
• tendsto_nhds: 終域側が 𝓝 y の Tendsto を開集合で読む．
• hf.continuousAt: 大域的連続性から点での連続性を得る．
• hg.comp hf: 連続写像の合成が連続であることを使う．

ここで Continuous.comp は，Continuous の field ではなく， 連続写像の合成が連続であることを述べる定理です． hg.comp hf のように書くとメソッドのように見えますが， Lean では名前空間 Continuous にある定理をドット notation で適用している，と読むとよいです． 一方，Continuous の定義の中で宣言されている成分，たとえば開集合の逆像が開集合であることを表す成分は field です．

#check Continuous
#check ContinuousAt
#check ContinuousOn
#check continuousAt_def
#check tendsto_nhds
#check Continuous.isOpen_preimage
#check Continuous.comp

section Continuity

variable {X Y Z : Type*}
variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]

example {f : X → Y} {x : X} :
    ContinuousAt f x = Tendsto f (𝓝 x) (𝓝 (f x)) := by
  rfl

example {f : X → Y} {x : X} :
    ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x := by
  exact continuousAt_def

example {α : Type*} {f : α → Y} {l : Filter α} {y : Y} :
    Tendsto f l (𝓝 y) ↔ ∀ s : Set Y, IsOpen s → y ∈ s → f ⁻¹' s ∈ l := by
  exact tendsto_nhds

example {f : X → Y} (hf : Continuous f) (x : X) : ContinuousAt f x := by
  exact hf.continuousAt

example {f : X → Y} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun x => g (f x) := by
  exact hg.comp hf

end Continuity