]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/igft/cantor.ma
LAMBDA-TYPES: mma's recommitted because inline syntax changed
[helm.git] / helm / software / matita / contribs / igft / cantor.ma
1 include "logic/cprop_connectives.ma".
2 include "igft.ma".
3
4 axiom A: Type.
5 axiom S_: A → Ω^A.
6
7 inductive Unit : Type := unit : Unit.
8
9 definition axs: AxiomSet.
10  constructor 1;
11   [ apply A;
12   | intro; apply Unit;
13   | intros; apply (S_ a)]
14 qed.
15
16 definition S : axs → Ω^axs ≝ S_.
17
18 definition emptyset: Ω^axs ≝ {x | False}.
19
20 notation "∅︀" non associative with precedence 90 for @{'emptyset}.
21 interpretation "emptyset" 'emptyset = emptyset.
22 notation "∅" non associative with precedence 91 for @{'emptyset1}.
23 interpretation "emptyset1" 'emptyset1 = emptyset.
24
25 definition Z: Ω \sup axs ≝ {x | x ⊲ ∅}.
26
27 theorem cantor: ∀a:axs. ¬ (Z ⊆ S a ∧ S a ⊆ Z).
28  intros 2; cases H; clear H;
29  cut (a ⊲ S a);
30   [2: apply infinity; [apply unit] change with (S a ⊲ S a); 
31       intros 2; apply refl; apply H;]
32  cut (a ⊲ ∅︀);
33   [2: apply (trans (S a)); [ assumption ]
34       intros 2; lapply (H2 ? H) as K;
35       change in K with (x ⊲ ∅ );
36       assumption;]
37  cut (a ε S a);
38   [2: apply H1; apply Hcut1;]
39  generalize in match Hcut2; clear Hcut2;
40  elim Hcut1 using covers_elim;
41   [ intros 2; cases H;
42   | intros; apply (H3 a1); [apply H4|apply H4]]
43 qed.