Skip to content

Instantly share code, notes, and snippets.

@pedrominicz

pedrominicz/Choice.v

Created April 2, 2020 20:14
Show Gist options
  • Save pedrominicz/0a974b41e95d99ea040a7bfcade47b53 to your computer and use it in GitHub Desktop.
Save pedrominicz/0a974b41e95d99ea040a7bfcade47b53 to your computer and use it in GitHub Desktop.
Download ZIP
The Axiom of Countable Choice
Raw
Choice.v
Theorem acc : forall {X : Type} {R : nat -> X -> Prop},
(forall n, { x & R n x }) -> { f & forall n, R n (f n) }.
Proof.
intros X R f.
exists (fun n => projT1 (f n)).
intros.
destruct (f n).
assumption.
Qed.
Theorem acc' : forall {X : Prop} {R : nat -> X -> Prop},
(forall n, exists x, R n x) -> exists (f : nat -> X), forall n, R n (f n).
Proof.
intros X R f.
exists (fun n => ex_proj1 (f n)).
intros.
destruct (f n).
assumption.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment