Zulip Chat Archive

Stream: Is there code for X?

Topic: axiom of choice for finite collections?


view this post on Zulip Alex Kontorovich (Mar 29 2021 at 17:16):

Hello, is there code that proves the axiom of choice for finite collections that doesn't invoke the infinite axiom of choice? Thanks!

view this post on Zulip Bryan Gin-ge Chen (Mar 29 2021 at 17:38):

You might need your collection to be docs#encodable if you really want to avoid choice.

view this post on Zulip Adam Topaz (Mar 29 2021 at 17:39):

Maybe docs#fintype.choose

view this post on Zulip Bhavik Mehta (Mar 29 2021 at 17:53):

Or docs#finset.choose

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 20:10):

You get two answers because you didn't formalise your question with a #mwe ;-)


Last updated: May 07 2021 at 22:14 UTC