一意選択公理

Definite descriptionという公理から一意選択公理が成り立つことを示す。

From Stdlib Require Import Logic.Description.

Check constructive_definite_description.
constructive_definite_description
     : forall (A : Type) (P : A -> Prop),
       (exists ! x : A, P x) -> {x : A | P x}

Definite descriptionは一意存在の証明からその項を取り出すことができる。上記の A : Type は暗黙の引数である。

Section UniqueChoice.
  Variable A B : Type.

  Definition functional_definite_description :
    forall R : A -> B -> Prop,
    (forall x : A, exists! y : B, R x y)
    -> { f : A -> B | forall x : A, R x (f x)}.
A, B: Type
forall R : A -> B -> Prop,
(forall x : A, exists ! y : B, R x y) ->
{f : A -> B | forall x : A, R x (f x)}
  Proof.
A, B: Type
forall R : A -> B -> Prop,
(forall x : A, exists ! y : B, R x y) ->
{f : A -> B | forall x : A, R x (f x)}
    intros.
A, B: Type
R: A -> B -> Prop
H: forall x : A, exists ! y : B, R x y
{f : A -> B | forall x : A, R x (f x)}
    set (F :=
      fun a => constructive_definite_description (R a) (H a)
    ).
A, B: Type
R: A -> B -> Prop
H: forall x : A, exists ! y : B, R x y
F:= fun a : A => constructive_definite_description (R a) (H a): forall a : A, {x : B | R a x}
{f : A -> B | forall x : A, R x (f x)}
    exists (fun a => proj1_sig (F a)).
A, B: Type
R: A -> B -> Prop
H: forall x : A, exists ! y : B, R x y
F:= fun a : A => constructive_definite_description (R a) (H a): forall a : A, {x : B | R a x}
forall x : A, R x (proj1_sig (F x))
    intro a.
A, B: Type
R: A -> B -> Prop
H: forall x : A, exists ! y : B, R x y
F:= fun a : A => constructive_definite_description (R a) (H a): forall a : A, {x : B | R a x}
a: A
R a (proj1_sig (F a))
    exact (proj2_sig (F a)).
  Defined.

  Theorem unique_choice :
    forall R : A -> B -> Prop,
    (forall x : A, exists! y : B, R x y)
    -> exists f : A -> B, forall x : A, R x (f x).
A, B: Type
forall R : A -> B -> Prop,
(forall x : A, exists ! y : B, R x y) ->
exists f : A -> B, forall x : A, R x (f x)
  Proof.
A, B: Type
forall R : A -> B -> Prop,
(forall x : A, exists ! y : B, R x y) ->
exists f : A -> B, forall x : A, R x (f x)
    intros.
A, B: Type
R: A -> B -> Prop
H: forall x : A, exists ! y : B, R x y
exists f : A -> B, forall x : A, R x (f x)
    apply ex_of_sig.
A, B: Type
R: A -> B -> Prop
H: forall x : A, exists ! y : B, R x y
{f : A -> B | forall x : A, R x (f x)}
    apply functional_definite_description.
A, B: Type
R: A -> B -> Prop
H: forall x : A, exists ! y : B, R x y
forall x : A, exists ! y : B, R x y
    assumption.
  Qed.
End UniqueChoice.