具体的な連続性計算¶

実数上の初等関数の連続性は，continuity tactic で証明できることが多いです．失敗した場合は，Continuous.add，Continuous.mul，Continuous.comp などの補題を明示的に使います．

式が長くなる場合は，1 行で全部を書くよりも，中間事実に名前を付けると読みやすくなります．たとえば分数関数では，分子の連続性，分母の連続性，分母が 0 でないことを別々の have にします．数値計算や式変形が長い場合は，前節と同じようにその部分だけ calc に切り出せます．

section ConcreteContinuity

example : Continuous fun x : ℝ => x ^ 2 + 1 := by
  continuity

example : ContinuousAt (fun x : ℝ => Real.sin x + x ^ 2) (0 : ℝ) := by
  simpa using
    (Real.continuous_sin.continuousAt.add
      ((continuousAt_id : ContinuousAt (fun x : ℝ => x) 0).pow 2))

上の ContinuousAt の例では，Real.continuous_sin，continuousAt_id， .pow，.add を手で組み合わせています．大域的な連続性なら，同じ組み合わせを continuity に任せられることも多いです．たとえば，\(x \mapsto \sin x + x^2\) は次のように証明できます．

example : Continuous fun x : ℝ => Real.sin x + x ^ 2 := by
  continuity

分母を持つ関数では，分母が 0 でないことが必要です．一点での連続性なら，その点で分母が 0 でないことを示せば十分です．次は \(x=0\) における

\[ (x^2+1)/(x+3) \]

の連続性です．

example : ContinuousAt (fun x : ℝ => (x ^ 2 + 1) / (x + 3)) 0 := by
  have hnum : ContinuousAt (fun x : ℝ => x ^ 2 + 1) 0 :=
    ((continuousAt_id : ContinuousAt (fun x : ℝ => x) 0).pow 2).add continuousAt_const
  have hden : ContinuousAt (fun x : ℝ => x + 3) 0 :=
    (continuousAt_id : ContinuousAt (fun x : ℝ => x) 0).add continuousAt_const
  have hden0 : (0 : ℝ) + 3 ≠ 0 := by
    norm_num
  exact hnum.div hden hden0

大域的な連続性では，すべての点で分母が 0 でないことを示します．次の例では \(x^2+2>0\) なので分母は 0 になりません．

example : Continuous fun x : ℝ => (x ^ 2 + 1) / (x ^ 2 + 2) := by
  have hnum : Continuous fun x : ℝ => x ^ 2 + 1 :=
    ((continuous_id : Continuous fun x : ℝ => x).pow 2).add continuous_const
  have hden : Continuous fun x : ℝ => x ^ 2 + 2 :=
    ((continuous_id : Continuous fun x : ℝ => x).pow 2).add continuous_const
  have hden0 : ∀ x : ℝ, x ^ 2 + 2 ≠ 0 := by
    intro x
    positivity
  exact hnum.div hden hden0

end ConcreteContinuity

演習問題¶

開集合の連続写像による逆像が開集合であることを示してください．

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} (hf : Continuous f) {U : Set Y} (hU : IsOpen U) :
    IsOpen (f ⁻¹' U) := by
  -- `hU.preimage hf` を試す．
  -- 解答例: exact hU.preimage hf
  sorry

閉集合の連続写像による逆像が閉集合であることを示してください．

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} (hf : Continuous f) {C : Set Y} (hC : IsClosed C) :
    IsClosed (f ⁻¹' C) := by
  -- `hC.preimage hf` を試す．
  -- 解答例: exact hC.preimage hf
  sorry

実数値連続関数 f g : X → ℝ について，集合 {x | f x ≤ g x} が閉集合であることを示してください．

example {X : Type*} [TopologicalSpace X] {f g : X → ℝ}
    (hf : Continuous f) (hg : Continuous g) :
    IsClosed {x : X | f x ≤ g x} := by
  -- `isClosed_le hf hg` を調べる．
  -- 解答例: exact isClosed_le hf hg
  sorry

{x | f x < g x} が開集合であることを調べてください．

example {X : Type*} [TopologicalSpace X] {f g : X → ℝ}
    (hf : Continuous f) (hg : Continuous g) :
    IsOpen {x : X | f x < g x} := by
  -- `isOpen_lt hf hg` を調べる．
  -- 解答例: exact isOpen_lt hf hg
  sorry

ContinuousAt が Tendsto であることを確認してください．

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} {x : X} :
    ContinuousAt f x = Tendsto f (𝓝 x) (𝓝 (f x)) := by
  -- ヒント: `rfl`
  -- 解答例: rfl
  sorry