Аксиома choice в Lean действительно не совпадает с axiom of choice в теории множеств.Аксиома choice в Lean на самом деле не имеет соответствующего утверждения в теории множеств.Говорят, что есть функция , которая берет доказательство того, что какой-то тип α непуста, и производит жителя α.В теории множеств мы не можем определить функции, которые принимают доказательства в качестве аргументов, поскольку доказательства не являются объектами в теории множеств, они находятся в слое логики поверх всего этого.
Тем не менее, две аксиомы выбора не являютсясовершенно не связано.Из аксиомы Линса choice вы можете доказать более знакомую аксиому выбора из теории множеств, одну версию которой вы можете найти здесь .
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)
В других частях библиотеки доказаны другие эквивалентные утверждения аксиоме выбора, например, каждая сюръективная функция имеет правую обратную .
Может быть,Утверждение, наиболее близкое к приведенной вами версии аксиомы выбора, является следующим:
theorem axiom_of_choice' {α : Sort u} {β : α → Sort v} (h : ∀ x, nonempty (β x)) :
nonempty (Π x, β x) :=
⟨λ x, classical.choice (h x)⟩
На словах это говорит: для данного семейства непустых типов (множеств) тип функций выбора непустой.Как вы можете видеть, доказательство непосредственно из choice.
Лина.