距離空間での読み替え¶
距離空間や擬距離空間では，dist x y，開球 Metric.ball x ε，閉球 Metric.closedBall x ε などを使います．
距離空間は位相空間構造を誘導するため，距離の話から IsOpen や Continuous の話へ移れます．
また ContinuousAt のフィルターによる定義は，距離空間では通常の ε-δ 条件と同値になります．
#check PseudoMetricSpace
#check Metric.ball
#check Metric.closedBall
#check dist
#check Metric.continuousAt_iff
section MetricSpaces
open Metric
variable {X : Type*} [PseudoMetricSpace X]
example (x : X) : dist x x = 0 := by
simp
example (x y : X) : 0 ≤ dist x y := by
exact dist_nonneg
example (x : X) (ε : ℝ) (hε : 0 < ε) : x ∈ Metric.ball x ε := by
simpa [Metric.mem_ball] using hε
example (x : X) (ε : ℝ) : IsOpen (Metric.ball x ε) := by
exact Metric.isOpen_ball
end MetricSpaces
section MetricContinuity
example {f : ℝ → ℝ} {a : ℝ} :
ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℝ⦄,
dist x a < δ → dist (f x) (f a) < ε := by
exact Metric.continuousAt_iff
example : ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℝ⦄,
dist x 3 < δ → dist (x + 1) ((3 : ℝ) + 1) < ε := by
have h : ContinuousAt (fun y : ℝ => y + 1) (3 : ℝ) := by
exact (continuousAt_id : ContinuousAt (fun y : ℝ => y) 3).add continuousAt_const
exact Metric.continuousAt_iff.mp h
end MetricContinuity
Metric.ball x ε は集合です．
したがって x ∈ Metric.ball x ε や IsOpen (Metric.ball x ε) のように，集合に関する命題として扱えます．
Metric.continuousAt_iff を使うと，具体的な関数の連続性から
ε-δ 条件を取り出せます．
上の例は \(x \mapsto x+1\) が \(x=3\) で連続であることを，
距離による条件として読み替えています．
ここに現れる ∀ ⦃x : ℝ⦄, ... の ⦃x : ℝ⦄ は strict implicit binder です．
x 自体は普通の実数の点ですが，定理を使うときには明示的に渡さず，
後続の仮定 dist x a < δ などから Lean が推論します．
たとえば h : ∀ ⦃x : ℝ⦄, dist x a < δ → ... があるとき，
h hx のように書くと，hx の型から x が推論されます．
構文としては {{x : ℝ}} と入力でき，表示上は ⦃x : ℝ⦄ になります．
括弧の種類の一般的な説明は基礎編 Chapter 02 の variable と引数の節で扱いました．
演習問題¶
-
距離空間で，開球が開集合であることをもう一度証明してください．
-
距離空間で，
ContinuousAtがε-δ条件と同値であることを確認してください．