编辑“︁Lean序理论”︁（章节）

== 基本定义 ==

=== 偏序（Partial Order） ===
在数学中，'''偏序集'''（Partially Ordered Set, Poset）是一个集合<math>P</math>配上一个二元关系<math>\leq</math>，满足以下性质：
* '''自反性'''：<math>\forall x \in P, x \leq x</math>
* '''反对称性'''：<math>\forall x, y \in P, x \leq y \land y \leq x \implies x = y</math>
* '''传递性'''：<math>\forall x, y, z \in P, x \leq y \land y \leq z \implies x \leq z</math>

在Lean中，偏序通过类型类`Preorder`和`PartialOrder`定义：
<syntaxhighlight lang="lean">
class Preorder (α : Type u) extends LE α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c

class PartialOrder (α : Type u) extends Preorder α where
  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
</syntaxhighlight>

=== 全序（Total Order） ===
'''全序'''是偏序的特殊情况，要求任意两个元素都是可比较的：
* '''全序性'''：<math>\forall x, y \in P, x \leq y \lor y \leq x</math>

Lean中的定义：
<syntaxhighlight lang="lean">
class LinearOrder (α : Type u) extends PartialOrder α where
  le_total : ∀ a b : α, a ≤ b ∨ b ≤ a
</syntaxhighlight>