编辑“︁Lean蕴含关系”︁（章节）

== 基本使用 ==

在Lean中，我们可以直接使用 `→` 来构造蕴含命题：

<syntaxhighlight lang="lean">
example : (P → Q) → (Q → R) → (P → R) :=
  fun hPQ hQR hP => hQR (hPQ hP)
</syntaxhighlight>

这个例子展示了“如果P蕴含Q，且Q蕴含R，那么P蕴含R”的传递性。代码解释：
1. `hPQ : P → Q` 是第一个假设。
2. `hQR : Q → R` 是第二个假设。
3. `hP : P` 是第三个假设。
4. `hPQ hP` 应用第一个假设到 `hP`，得到 `Q`。
5. `hQR (hPQ hP)` 应用第二个假设到上一步的结果，得到 `R`。