Library Continuum.Sierpinskis_Theorem
Require Export Continuum.Hartogs_Number.
Require Import Coq.Logic.Classical.
Require Import Coq.Program.Program.
Require Import Coq.Init.Nat.
Definition Infinite (A : S) :=
Numeral ≤ A.
Definition Generalized_Continuum_Hypothesis :=
∀ x y : S,
Infinite x →
x ≤ y ≤ 𝒫 x →
x = y ∨ y = 𝒫 x.
Definition Well_Ordering_Theorem :=
∀ x : S, inhabited (Well_Order_On x).
Definition Axiom_Of_Choice' :=
∀ (I : S) (F : I → S),
inhabited (∀ i, inhabited (F i) → F i).
Definition Axiom_Of_Choice :=
∀ (I : S) (F : I → S),
(∀ i, inhabited (F i)) →
inhabited (∀ i, F i).
Goal Axiom_Of_Choice → Axiom_Of_Choice'.
intros ac I F.
unshelve eset (H := ac `{i in I | inhabited (F i)}
(fun i ⇒ F (element i))
_). {
cbn. intros i. apply (comprehension_condition i).
} destruct H as [f].
apply inhabits.
intros i Hi.
assert (i ∈ `{ i in I | inhabited (F i)}). {
rewrite in_comprehension_iff_typed. assumption.
}
specialize (f (element i)).
cbn in f. rewrite strip_element in f. exact f.
Qed.
Theorem Well_Ordering_to_Choice :
Well_Ordering_Theorem → Axiom_Of_Choice.
Proof.
intros well_ordering I F H.
destruct (well_ordering (⋃ i ∈ I, F i)) as [R].
apply inhabits.
assert (∀ i, F i ∈ 𝒫 (⋃ i ∈ I, F i)) by automation.
exact (fun i ⇒ least_element (element (F i)) (H i)).
Qed.
Lemma lemma1 (A B : S) :
A ⊔ A ∼ A →
A ⊔ B ∼ 𝒫 A →
𝒫 A ≤ B.
Proof.
intros H1 H2.
assert (f : A ⊔ B ∼ 𝒫 A × 𝒫 A). {
transitivity (𝒫 A). {
exact H2.
}
transitivity (𝒫 (A ⊔ A)). {
rewrite H1. reflexivity.
}
rewrite power_set_of_disjoint_union. reflexivity.
} destruct f as [f].
clear H1 H2.
assert (H : ∃ A1 : 𝒫 A, ∀ A2 : 𝒫 A, (f⁻¹ `(A1, A2)).(Is_From_Right)). {
set (g := π1 ∘ f ∘ inj1 _ _ : A → 𝒫 A).
assert (H : ¬ g.(Is_Surjective)). {
intros H. apply (cantors_theorem A).
exact (inhabits (build_surjection g H)).
}
change (¬ ∀ A1, ∃ a, A1 = g a) in H.
apply not_all_ex_not in H. destruct H as [A1 H]. ∃ A1.
intros A2.
enough (¬ (f⁻¹ `(A1, A2)).(Is_From_Left)). {
destruct (from_left_or_right (f⁻¹ `(A1, A2))); tauto.
}
unfold Is_From_Left. unfold g in H; cbn in g.
intros [a contra]. apply H. ∃ a.
unfold compose. rewrite <- contra.
rewrite cancel_inverse_right. rewrite left_projection_beta.
reflexivity.
}
destruct H as [A1 H].
unshelve eset (g (A2 : 𝒫 A) := extract_from_right (f⁻¹ `(A1, A2)) : B). {
apply H.
}
simple refine (inhabits (build_injection g _)).
intros A2 A2' H1. unfold g in H1.
apply extract_from_right_is_injective in H1.
apply bijection_is_injective in H1.
apply pair_is_injective_right in H1.
exact H1.
Qed.
Lemma lemma2 (x y : S) :
Generalized_Continuum_Hypothesis →
Infinite x →
x ⊔ x ∼ x →
𝒫 x ⊔ 𝒫 x ∼ 𝒫 x →
y ≤ 𝒫 x →
y ≤ x ∨ 𝒫 x ≤ y.
Proof.
intros gch. intros H1 H2 H3 H4.
assert (x ≤ x ⊔ y ≤ 𝒫 x). {
split.
- apply disjoint_union_is_increasing_on_left.
- rewrite (power_set_is_increasing x) at 1.
rewrite H4. rewrite H3. reflexivity.
}
assert (cases : x = x ⊔ y ∨
x ⊔ y = 𝒫 x). {
apply gch; assumption.
} destruct cases as [-> | H5].
- left. apply disjoint_union_is_increasing_on_right.
- right. apply lemma1.
+ assumption.
+ rewrite H5. reflexivity.
Qed.
Theorem sierpinskis_theorem :
Generalized_Continuum_Hypothesis → Axiom_Of_Choice.
Proof.
intros gch. apply Well_Ordering_to_Choice. intros x.
enough (H : ∃ O : Ordinal, x ≤ O). {
destruct H as [O [f]].
apply inhabits.
apply (transport_well_order (injection_as_bijection_into_image f)⁻¹).
exact (restrict_well_order (ordinal_order O) (image_of f)).
}
set (x0 := x ⊔ Numeral).
set (x' n := iter (1 + n) 𝒫 x0).
∃ (hartogs_number (x' 0)).
transitivity (x' 0). {
cbn. unfold x0.
rewrite <- power_set_is_increasing.
rewrite <- disjoint_union_is_increasing_on_left.
reflexivity.
}
assert (H1 : ∀ n, x' n ⊔ x' n ∼ x' n). {
intros n. change (x' n) with (𝒫 (iter n 𝒫 x0)).
symmetry. apply power_set_equiv_power_set_plus_power_set.
induction n.
- cbn. unfold x0. apply disjoint_union_is_increasing_on_right.
- change (iter (Datatypes.S n) 𝒫 x0) with (𝒫 (iter n 𝒫 x0)).
rewrite power_set_is_increasing at 1. rewrite IHn at 1. reflexivity.
}
assert (H2 : (hartogs_number (x' 0) : S) ≤ x' 6) by
apply hartogs_number_has_upper_bound.
revert H2. generalize 6. intros n H2. induction n.
- apply hartogs_number_is_not_smaller in H2. contradiction.
- assert (cases : (hartogs_number (x' 0) : S) ≤ x' n ∨
x' (1 + n) ≤ hartogs_number (x' 0)). {
apply lemma2; auto.
- unfold Infinite. clear. induction n.
+ cbn. unfold x0. rewrite <- power_set_is_increasing.
apply disjoint_union_is_increasing_on_right.
+ change (Numeral ≤ 𝒫 (x' n)).
rewrite IHn. apply power_set_is_increasing.
- apply H1.
} destruct cases as [ | <-].
+ apply IHn. assumption.
+ unfold x'. generalize (1 + n) x0; clear. intros n x0; induction n.
× reflexivity.
× rewrite IHn. rewrite power_set_is_increasing. reflexivity.
Qed.
Require Import Coq.Logic.Classical.
Require Import Coq.Program.Program.
Require Import Coq.Init.Nat.
Definition Infinite (A : S) :=
Numeral ≤ A.
Definition Generalized_Continuum_Hypothesis :=
∀ x y : S,
Infinite x →
x ≤ y ≤ 𝒫 x →
x = y ∨ y = 𝒫 x.
Definition Well_Ordering_Theorem :=
∀ x : S, inhabited (Well_Order_On x).
Definition Axiom_Of_Choice' :=
∀ (I : S) (F : I → S),
inhabited (∀ i, inhabited (F i) → F i).
Definition Axiom_Of_Choice :=
∀ (I : S) (F : I → S),
(∀ i, inhabited (F i)) →
inhabited (∀ i, F i).
Goal Axiom_Of_Choice → Axiom_Of_Choice'.
intros ac I F.
unshelve eset (H := ac `{i in I | inhabited (F i)}
(fun i ⇒ F (element i))
_). {
cbn. intros i. apply (comprehension_condition i).
} destruct H as [f].
apply inhabits.
intros i Hi.
assert (i ∈ `{ i in I | inhabited (F i)}). {
rewrite in_comprehension_iff_typed. assumption.
}
specialize (f (element i)).
cbn in f. rewrite strip_element in f. exact f.
Qed.
Theorem Well_Ordering_to_Choice :
Well_Ordering_Theorem → Axiom_Of_Choice.
Proof.
intros well_ordering I F H.
destruct (well_ordering (⋃ i ∈ I, F i)) as [R].
apply inhabits.
assert (∀ i, F i ∈ 𝒫 (⋃ i ∈ I, F i)) by automation.
exact (fun i ⇒ least_element (element (F i)) (H i)).
Qed.
Lemma lemma1 (A B : S) :
A ⊔ A ∼ A →
A ⊔ B ∼ 𝒫 A →
𝒫 A ≤ B.
Proof.
intros H1 H2.
assert (f : A ⊔ B ∼ 𝒫 A × 𝒫 A). {
transitivity (𝒫 A). {
exact H2.
}
transitivity (𝒫 (A ⊔ A)). {
rewrite H1. reflexivity.
}
rewrite power_set_of_disjoint_union. reflexivity.
} destruct f as [f].
clear H1 H2.
assert (H : ∃ A1 : 𝒫 A, ∀ A2 : 𝒫 A, (f⁻¹ `(A1, A2)).(Is_From_Right)). {
set (g := π1 ∘ f ∘ inj1 _ _ : A → 𝒫 A).
assert (H : ¬ g.(Is_Surjective)). {
intros H. apply (cantors_theorem A).
exact (inhabits (build_surjection g H)).
}
change (¬ ∀ A1, ∃ a, A1 = g a) in H.
apply not_all_ex_not in H. destruct H as [A1 H]. ∃ A1.
intros A2.
enough (¬ (f⁻¹ `(A1, A2)).(Is_From_Left)). {
destruct (from_left_or_right (f⁻¹ `(A1, A2))); tauto.
}
unfold Is_From_Left. unfold g in H; cbn in g.
intros [a contra]. apply H. ∃ a.
unfold compose. rewrite <- contra.
rewrite cancel_inverse_right. rewrite left_projection_beta.
reflexivity.
}
destruct H as [A1 H].
unshelve eset (g (A2 : 𝒫 A) := extract_from_right (f⁻¹ `(A1, A2)) : B). {
apply H.
}
simple refine (inhabits (build_injection g _)).
intros A2 A2' H1. unfold g in H1.
apply extract_from_right_is_injective in H1.
apply bijection_is_injective in H1.
apply pair_is_injective_right in H1.
exact H1.
Qed.
Lemma lemma2 (x y : S) :
Generalized_Continuum_Hypothesis →
Infinite x →
x ⊔ x ∼ x →
𝒫 x ⊔ 𝒫 x ∼ 𝒫 x →
y ≤ 𝒫 x →
y ≤ x ∨ 𝒫 x ≤ y.
Proof.
intros gch. intros H1 H2 H3 H4.
assert (x ≤ x ⊔ y ≤ 𝒫 x). {
split.
- apply disjoint_union_is_increasing_on_left.
- rewrite (power_set_is_increasing x) at 1.
rewrite H4. rewrite H3. reflexivity.
}
assert (cases : x = x ⊔ y ∨
x ⊔ y = 𝒫 x). {
apply gch; assumption.
} destruct cases as [-> | H5].
- left. apply disjoint_union_is_increasing_on_right.
- right. apply lemma1.
+ assumption.
+ rewrite H5. reflexivity.
Qed.
Theorem sierpinskis_theorem :
Generalized_Continuum_Hypothesis → Axiom_Of_Choice.
Proof.
intros gch. apply Well_Ordering_to_Choice. intros x.
enough (H : ∃ O : Ordinal, x ≤ O). {
destruct H as [O [f]].
apply inhabits.
apply (transport_well_order (injection_as_bijection_into_image f)⁻¹).
exact (restrict_well_order (ordinal_order O) (image_of f)).
}
set (x0 := x ⊔ Numeral).
set (x' n := iter (1 + n) 𝒫 x0).
∃ (hartogs_number (x' 0)).
transitivity (x' 0). {
cbn. unfold x0.
rewrite <- power_set_is_increasing.
rewrite <- disjoint_union_is_increasing_on_left.
reflexivity.
}
assert (H1 : ∀ n, x' n ⊔ x' n ∼ x' n). {
intros n. change (x' n) with (𝒫 (iter n 𝒫 x0)).
symmetry. apply power_set_equiv_power_set_plus_power_set.
induction n.
- cbn. unfold x0. apply disjoint_union_is_increasing_on_right.
- change (iter (Datatypes.S n) 𝒫 x0) with (𝒫 (iter n 𝒫 x0)).
rewrite power_set_is_increasing at 1. rewrite IHn at 1. reflexivity.
}
assert (H2 : (hartogs_number (x' 0) : S) ≤ x' 6) by
apply hartogs_number_has_upper_bound.
revert H2. generalize 6. intros n H2. induction n.
- apply hartogs_number_is_not_smaller in H2. contradiction.
- assert (cases : (hartogs_number (x' 0) : S) ≤ x' n ∨
x' (1 + n) ≤ hartogs_number (x' 0)). {
apply lemma2; auto.
- unfold Infinite. clear. induction n.
+ cbn. unfold x0. rewrite <- power_set_is_increasing.
apply disjoint_union_is_increasing_on_right.
+ change (Numeral ≤ 𝒫 (x' n)).
rewrite IHn. apply power_set_is_increasing.
- apply H1.
} destruct cases as [ | <-].
+ apply IHn. assumption.
+ unfold x'. generalize (1 + n) x0; clear. intros n x0; induction n.
× reflexivity.
× rewrite IHn. rewrite power_set_is_increasing. reflexivity.
Qed.