Zulip Chat Archive

Stream: new members

Topic: choose tactic

abaaba (Oct 14 2021 at 08:24):

I couldn't see how this do with axiom of choice ... neither can I understand its meaning ....

Mario Carneiro (Oct 14 2021 at 08:25):

tactic#choose is probably easier to read

Mario Carneiro (Oct 14 2021 at 08:27):

If you have a theorem h saying that for all x : A, there exists y : B such that P x y, then choose h with f h' produces f : A -> B and h' saying that P x (f x). That's the axiom of choice

Mario Carneiro (Oct 14 2021 at 08:27):

here f is the set of choices, one y for each x

abaaba (Oct 14 2021 at 08:29):

I think it would make sense to me if A is restricted to Set X, and y is of type X. But how does it generalize to other types?

Mario Carneiro (Oct 14 2021 at 08:40):

This is maybe not exactly the version of the axiom of choice that you are thinking of. Here's the version from wikipedia that gets pretty close to the type theory version:

In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that a Cartesian product of a collection of non-empty sets is non-empty. Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin, even if the collection is infinite. Formally, it states that for every indexed family (Si)iI(S_{i})_{i\in I} of nonempty sets there exists an indexed family (xi)iI(x_{i})_{i\in I} of elements such that xiSix_{i}\in S_{i} for every iIi\in I.

Mario Carneiro (Oct 14 2021 at 08:42):

To map this to the version I just said, let II be A, and let SiS_i be {y : B // P i y}

Mario Carneiro (Oct 14 2021 at 08:44):

The family λ x, {y : B // P x y} is a family of nonempty sets, because for every x there exists y such that P x y, and the resulting indexed family (xi)iI(x_i)_{i\in I} is f, or more precisely λ x, ⟨f x, h' x⟩; for each x, f x : B and h' x : P x (f x) so ⟨f x, h' x⟩ : {y : B // P x y} as desired.

Last updated: Dec 20 2023 at 11:08 UTC