import GlimpseOfLean.Library.Basic

namespace Introduction

本教程的介绍

如果你的屏幕较小且正在 VSCode 中阅读此文件，你可以按下 alt-Z（或 option-Z）来启用自动换行。

欢迎来到这个设计用于让你在几小时内一窥 Lean 的教程。

首先让我们看看 Lean 证明长什么样子，暂时不用理解任何语法细节。你不需要在这个文件中输入任何内容。

如果一切正常，你现在应该在文本右边看到一个面板，显示类似"No info found."的消息。这个面板将在证明内部开始显示有趣的内容。

请注意，任何在 /- 和 `

` 之间或在 `--` 之后的文本都是注释是为你准备的，Lean 会忽略这些内容。

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

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

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

在上面的定义中，注意序列 u 的第 n 项简单地记作 u n。

类似地，在下一个定义中，f x 就是我们在纸上写的 f(x)。另请注意，蕴含用单箭头表示（我们稍后会解释原因）。

更加微妙的是，我们写 l : ℝ 来表示 l 是一个实数，而你在纸上可能会写 l ∈ ℝ。

我们称函数 f : ℝ → ℝ 在 x₀ 处连续，若 ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ ⇒ |f(x) - f(x₀)| ≤ ε。这个条件将写作 continuous_at f x₀。

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

现在我们声明，如果 f 在 x₀ 处连续，那么它在 x₀ 处序列连续：对于任何收敛到 x₀ 的序列 u，序列 f ∘ u 收敛到 f x₀。下一行的所有内容都描述了对象和假设，每个都有其名称。接下来的行是我们需要证明的断言。

example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ) (hu : seq_limit u x₀) (hf : continuous_at f x₀) :
  seq_limit (f ∘ u) (f x₀) := by -- 这个 `by` 关键字标志着证明的开始
  -- 将你的文本光标放在这里并观察右侧的面板。
  -- 蓝色 `⊢` 符号右边是我们试图证明的内容。在此之上
  -- 是我们的变量和假设列表。当你阅读证明时，将光标从一行移动到另一行
  -- （例如使用下箭头键）并观察面板的变化。

  -- 我们的目标是证明，对于任何正数 `ε`，存在一个自然数
  -- `N`，使得对于任何至少为 `N` 的自然数 `n`，
  -- `|f(u_n) - f(x₀)|` 至多为 `ε`。
  unfold seq_limit
  -- 固定一个正数 `ε`。
  intros ε hε
  -- 根据关于 `f` 应用于这个正数 `ε` 的假设，我们得到一个正数 `δ`
  -- `Hf`: 使得对于所有实数 `x`，如果 `|x - x₀| ≤ δ`，那么 `|f(x) - f(x₀)| ≤ ε` (1)。
  obtain ⟨δ, δ_pos, Hf⟩ : ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε := hf ε hε
  -- 关于 `u` 应用于这个 `δ` 的假设给出一个自然数 `N`，使得
  -- `Hu`: 对于每个自然数 `n`，如果 `n ≥ N`，那么 `|u_n - x₀| ≤ δ`   (2)。
  obtain ⟨N, Hu⟩ : ∃ N, ∀ n ≥ N, |u n - x₀| ≤ δ := hu δ δ_pos
  -- 让我们证明 `N` 即为所求。
  use N
  -- 对于任意 `n`，满足 `n ≥ N`，我们证明 `|f(u_n) - f(x₀)| ≤ ε`。
  intros n hn
  -- 将 (1) 应用于 `u_n`，我们只需要证明 `|u_n - x₀| ≤ δ`。
  apply Hf
  -- 由性质 (2) 和我们关于 `n` 的假设立得。
  apply Hu n hn
  -- 证明完成！

现在这个证明结束了，你可以选择短版路径或长版路径。如果你想在 lean4web 服务器上做短版路径，你应该访问 https://live.lean-lang.org/#project=GlimpseOfLean&url=https%3A%2F%2Fraw.githubusercontent.com%2FPatrickMassot%2FGlimpseOfLean%2Frefs%2Fheads%2Fmaster%2FGlimpseOfLean%2FExercises%2FShorter.lean。

如果你使用本地安装或 GitPod 或 Codespaces 跟随长版路径，你应该使用此面板左侧的文件浏览器打开文件 Exercises > 01Rewriting.lean。