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

== 格理论 ==

格（Lattice）是一种特殊的偏序集，其中任意两个元素都有最小上界（join）和最大下界（meet）。

=== 格的定义 ===
在Lean中，格可以通过以下方式定义：
<syntaxhighlight lang="lean">
class Lattice (α : Type u) extends PartialOrder α where
  sup : α → α → α
  inf : α → α → α
  le_sup_left : ∀ a b : α, a ≤ a ⊔ b
  le_sup_right : ∀ a b : α, b ≤ a ⊔ b
  sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c
  inf_le_left : ∀ a b : α, a ⊓ b ≤ a
  inf_le_right : ∀ a b : α, a ⊓ b ≤ b
  le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c
</syntaxhighlight>

=== 示例：自然数上的格 ===
自然数集<math>\mathbb{N}</math>关于通常的≤关系构成一个格，其中<math>a \sqcup b = \max(a,b)</math>，<math>a \sqcap b = \min(a,b)</math>。

在Lean中的实现：
<syntaxhighlight lang="lean">
instance : Lattice ℕ where
  le := Nat.le
  le_refl := Nat.le_refl
  le_trans := @Nat.le_trans
  le_antisymm := @Nat.le_antisymm
  sup := max
  inf := min
  le_sup_left := Nat.le_max_left
  le_sup_right := Nat.le_max_right
  sup_le := fun a b c => Nat.max_le.2
  inf_le_left := Nat.min_le_left
  inf_le_right := Nat.min_le_right
  le_inf := fun a b c => Nat.le_min.2
</syntaxhighlight>