import GlimpseOfLean.Library.Basic

namespace Introduction

LEAN 教程简介

如果您使用的是小屏幕，可以按下 alt-Z（或option-Z）键来启用自动换行。

欢迎来到这个旨在在几个小时内让您对 LEAN 有所了解的教程。

首先让我们看一下一个 LEAN 证明的样子，暂时不需要理解其中的语法细节。您不需要在此文件中输入任何内容。

如果一切正常，您当前应该看到本文右侧一个名为“Lean Infoview”的面板，上面显示着“No info found.”之类的消息。这个面板将开始显示证明中的有趣内容。

首先让我们回顾两个微积分定义。

如果一个实数序列 u 收敛到 l ，则对于任意 ε > 0 ，存在一个 N ，使得对于所有 n ≥ N ，都满足 |uₙ - l| ≤ ε。我们将这个条件写作 seq_limit u l。

def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε

在上面的定义中，注意到序列 u 的第 n 项简单地表示为 u n。

类似地，在下一个定义中，f x 可以写作在纸上我们会写作 f(x)。还要注意，蕴含关系使用单箭头表示（稍后我们会解释原因）。

如果一个函数 f: ℝ → ℝ 在 x₀ 处连续，则对于任意 ε > 0 ，存在一个 δ > 0 ，使得对于所有 x ，只要 |x - x₀| ≤ δ ，就有 |f(x) - f(x₀)| ≤ ε。我们将这个条件写作 continuous_at f x₀。

def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) : Prop :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε

现在我们声称，如果 f 在 x₀ 处连续，则它在 x₀ 处是顺序连续的：对于任意收敛到 x₀ 的序列 u ，序列 f ∘ u 收敛

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ) (hu : seq_limit u x₀) (hf : continuous_at f x₀) :
  seq_limit (f ∘ u) (f x₀) := by { -- 这里的 `by` 关键字标志着开始证明的地方
  -- 将光标放在这里，观察右侧的 Lean InfoView 面板。
  -- 在证明的过程中，根据需要将光标从一行移动到另一行，同时监视 InfoView 面板。

  -- 我们的目标是证明，对于任意正的 `ε` ，存在一个自然数 `N` ，使得对于任意自然数 `n` ，如果 `n ≥ N` ，则 `|f(u_n) - f(x₀)|` 至多为 `ε`。
  unfold seq_limit
  -- 取一个正的数 `ε`。
  intros ε hε
  -- 根据 `f` 在这个正的 `ε` 上的假设，我们得到一个正的 `δ` ，使得对于所有实数 `x` ，如果 `|x - x₀| ≤ δ` ，则 `|f(x) - f(x₀)| ≤ ε` (1)。
  obtain ⟨δ, δ_pos, Hf⟩ : ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε := hf ε hε
  -- 根据 `u` 在这个 `δ` 上的假设，我们得到一个自然数 `N` ，使得对于每个自然数 `n` ，如果 `n ≥ N` ，则 `|u_n - x₀| ≤ δ` (2)。
  obtain ⟨N, Hu⟩ : ∃ N, ∀ n ≥ N, |u n - x₀| ≤ δ := hu δ δ_pos
  -- 我们证明 `N` 是合适的。
  use N
  -- 取一个大于等于 `N` 的 `n` 。我们证明 `|f(u_n) - f(x₀)| ≤ ε`。
  intros n hn
  -- 根据 (1) 对 `u_n` 的应用，我们只需证明 `|u_n - x₀| ≤ δ`。
  apply Hf
  -- 这可以通过 (2) 的性质以及我们对 `n` 的假设得到。
  exact Hu n hn
  -- 证明结束！
  }

现在此证明已经结束，您可以使用面板左侧的文件浏览器打开文件Exercises > 01Rewriting.lean。