coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem)

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem)
Date: Mon, 12 Sep 2016 15:53:06 +0200

On Mon, Sep 12, 2016 at 11:55:35AM +0200, Guillaume Melquiond wrote:

> This seems too strong. If I remember correctly, for Banach-Tarski, you
> just need a set S such that
>
> forall x, exists! y, S y /\ same_orbit x y.
> So you don't need the functional choice.

You made a formal proof? There is already a formal proof somewhere?

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

[Coq-Club] well-ordering axiom (aka Zermelo's theorem), Daniel de Rauglaudre, 09/12/2016
- Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem), Guillaume Melquiond, 09/12/2016
  - Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem), Daniel de Rauglaudre, 09/12/2016
- Re: [Coq-Club] well-ordering axiom (aka Zermelo's theorem), Daniel Schepler, 09/12/2016