精益中选择的定义
Definition of choice in Lean
在Lean中`choice'是根据：
实现的
我们的选择公理现在可以简单地表达如下：
axiom choice {α : Sort u} : nonempty α → α
仅给定 α 非空的断言 h，选择 h 神奇地产生了 α 的一个元素。
现在，如果我阅读有关集合论和选择公理的文献 (Jech)：
选择公理 (AC)。每个非空集合族都有一个选择函数。
如果 S 是集合族且 ∅ 不在 S 中，则 S 的选择函数是 S 上的函数 f 使得
f(X) ∈ X
对于每个 X ∈ S.
对我来说，这些东西似乎并不等同。有人可以详细说明一下吗？
精益中的公理choice确实和集合论中的axiom of choice不一样。 Lean 中的公理 choice 在集合论中并没有真正对应的陈述。所说的是有一个 函数 证明某些类型 α 是非空的，并产生一个 α 的居民。在集合论中，我们不能定义以证明为参数的函数，因为证明不是集合论中的对象，它们位于集合论之上的逻辑层中。
也就是说，这两个选择公理并非完全无关。从 Leans 公理 choice 你可以证明更熟悉的选择公理来自集合论，你可以找到一个版本 here。
theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
∃ (f : Π x, β x), ∀ x, r x (f x)
在库的其他部分中，证明了选择公理的其他等效语句，例如 every surjective function has a right inverse。
也许最接近您引用的选择公理版本的陈述如下：
theorem axiom_of_choice' {α : Sort u} {β : α → Sort v} (h : ∀ x, nonempty (β x)) :
nonempty (Π x, β x) :=
⟨λ x, classical.choice (h x)⟩
换句话说：给定一族非空类型（集合），选择函数的类型是非空的。如您所见，Lean 的 choice.
立即提供了证据
在Lean中`choice'是根据：
实现的我们的选择公理现在可以简单地表达如下：
axiom choice {α : Sort u} : nonempty α → α
仅给定 α 非空的断言 h，选择 h 神奇地产生了 α 的一个元素。
现在，如果我阅读有关集合论和选择公理的文献 (Jech)：
选择公理 (AC)。每个非空集合族都有一个选择函数。
如果 S 是集合族且 ∅ 不在 S 中，则 S 的选择函数是 S 上的函数 f 使得 f(X) ∈ X 对于每个 X ∈ S.
对我来说，这些东西似乎并不等同。有人可以详细说明一下吗？
精益中的公理choice确实和集合论中的axiom of choice不一样。 Lean 中的公理 choice 在集合论中并没有真正对应的陈述。所说的是有一个 函数 证明某些类型 α 是非空的，并产生一个 α 的居民。在集合论中，我们不能定义以证明为参数的函数，因为证明不是集合论中的对象，它们位于集合论之上的逻辑层中。
也就是说，这两个选择公理并非完全无关。从 Leans 公理 choice 你可以证明更熟悉的选择公理来自集合论，你可以找到一个版本 here。
theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
∃ (f : Π x, β x), ∀ x, r x (f x)
在库的其他部分中，证明了选择公理的其他等效语句，例如 every surjective function has a right inverse。
也许最接近您引用的选择公理版本的陈述如下：
theorem axiom_of_choice' {α : Sort u} {β : α → Sort v} (h : ∀ x, nonempty (β x)) :
nonempty (Π x, β x) :=
⟨λ x, classical.choice (h x)⟩
换句话说：给定一族非空类型（集合），选择函数的类型是非空的。如您所见，Lean 的 choice.