Аксиома choice в Lean действительно не то же самое, что axiom of choice в теории множеств. Аксиома choice в Lean на самом деле не имеет соответствующего утверждения в теории множеств. В нем говорится, что существует функция, которая принимает доказательство того, что некоторый тип α непустой, и производит жителя α. В теории множеств мы не можем определять функции, которые принимают доказательства в качестве аргументов, поскольку доказательства не являются объектами в теории множеств, они находятся на уровне логики поверх нее.
Тем не менее, две аксиомы выбора не совсем не связаны между собой. Из аксиомы Leans 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.
person
Floris van Doorn
schedule
29.03.2019
