集合的基本操作

Introduction

你已经掌握了命题逻辑的证明策略。从这一课开始，我们进入**集合论**。在 Lean 中，`Set α` 定义为 `α → Prop`——一个集合就是把每个元素映射到一个命题（「这个元素属于集合」是真还是假）。 `x ∈ A` 读作「x 属于 A」，本质上就是 `A x`——把 A 当作谓词应用到 x 上。本关目标：证明集合包含关系的**自反性**——任意集合都是自己的子集。即 `A ⊆ A`。你将学到： - `Set` 类型和 `∈` 符号的含义 - `⊆` 的定义：`A ⊆ B ↔ ∀ x, x ∈ A → x ∈ B` - 用 `intro` 展开定义，层层推进

本关学到的新东西

概念 (Concepts)

Set α类型 α 的集合，定义为 α → Prop。集合就是谓词

∈ (属于)x ∈ A 表示 x 是集合 A 的元素。本质上是 A x

⊆ (子集)A ⊆ B 定义为 ∀ x, x ∈ A → x ∈ B

证明目标

当前目标

A : Set Nat

⊢A ⊆ A

分步提示

1.`A ⊆ A` 的定义是 `∀ x, x ∈ A → x ∈ A`。所以先用 `intro x` 引入任意元素 x。
2.现在目标变成 `x ∈ A → x ∈ A`。这又是一个蕴涵，继续用 `intro hx`。hx 就是 `x ∈ A` 的证明。
3.目标现在是 `x ∈ A`。手里已经有 `hx : x ∈ A`，直接用 `exact hx`！
4.这个证明虽然简单，但它展示了集合论的核心模式：把集合关系展开成命题逻辑来处理。

怎么玩：编辑器里有预写代码。直接点 运行 ▶ 看效果，或修改代码后运行。卡住了看左侧的提示。

Lean 代码编辑器