3 include "topology/igft.ma".
5 ntheorem axiom_cond: âA:Ax.âa:A.âi:đ a.a â đ a i.
6 #A; #a; #i; @2 i; #x; #H; @; napply H;
9 nlemma hint_auto1 : âA,U,V. (âx.x â U â x â V) â cover_set cover A U V.
13 alias symbol "covers" (instance 1) = "covers".
14 alias symbol "covers" (instance 2) = "covers set".
15 alias symbol "covers" (instance 3) = "covers".
16 ntheorem transitivity: âA:Ax.âa:A.âU,V. a â U â U â V â a â V.
17 #A; #a; #U; #V; #aU; #UV;
20 ##| #c; #i; #HCU; #H; @2 i; nauto;
24 ndefinition emptyset: âA.Ί^A â ÎťA.{x | False}.
26 notation "â
" non associative with precedence 90 for @{ 'empty }.
27 interpretation "empty" 'empty = (emptyset ?).
29 naxiom EM : âA:Ax.âa:A.âi_star.(a â đ a i_star) ⨠( a â đ a i_star).
31 alias symbol "covers" = "covers".
33 âA:Ax.âa:A. a â â
â âi. ÂŹ a â đ a i.
36 ##| #b; #i_star; #IH1; #IH2;
37 ncases (EM ⌠b i_star);
38 ##[##2: (* nauto; *) #W; @i_star; napply W;
44 ninductive eq1 (A : Type[0]) : Type[0] â CProp[0] â
47 notation "hvbox( a break âź b)" non associative with precedence 40
50 interpretation "eq between types" 'eqT a b = (eq1 a b).
52 ninductive unit : Type[0] â one : unit.
54 nrecord uAx : Type[1] â {
56 with_ : âa:uax_.đ a âź unit
59 ndefinition uax : uAx â Ax.
60 #A; @ (uax_ A) (Îťx.unit); #a; #_; napply (đ a ?); nlapply one; ncases (with_ A a); nauto;
63 ncoercion uax : âu:uAx. Ax â uax on _u : uAx to Ax.
69 @; ##[ @ A (Îť_.unit) (Îťa,x.S a); ##| #_; @; ##]
72 alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
73 unification hint 0 â ;
75 (* -------------- *) â˘
80 âA:uAx.âa:A. a â â
â ÂŹ a â đ a ?. ##[ (* bug *) ##2: nnormalize; napply one; ##]
83 ##| #b; #i_star; #IH1; #IH2; #H3; nlapply (IH2 ⌠H3); #H4; nauto;
87 ndefinition Z : Ί^axs â { x | x â â
}.
89 ntheorem cover_monotone: âA:Ax.âa:A.âU,V.U â V â a â U â a â V.
90 #A; #a; #U; #V; #HUV; #H; nelim H;
92 ##| #b; #i; #HCU; #W; @2 i; #x; nauto; ##]
95 ntheorem th3_1: ÂŹâa:axs.Z â S a ⧠S a â Z.
98 nlapply (axiom_cond ⌠a one); #AxCon; nchange in AxCon with (a â S a);
99 (* nauto; *) napply (cover_monotone ⌠AxCon); nassumption; ##] #H;
100 ncut (a â â
); ##[ napply (transitivity ⌠H); #x; #E; napply E; ##] #H1;
101 ncut (ÂŹ a â S a); ##[ napply (col2_4 ⌠H1); ##] #H2;
102 ncut (a â S a); ##[ napply ZSa; napply H1; ##] #H3;
106 include "nat/nat.ma".
108 naxiom phi : nat â nat â nat.
110 notation > "Ď" non associative with precedence 90 for @{ 'phi }.
111 interpretation "phi" 'phi = phi.
113 notation < "Ď a i" non associative with precedence 90 for @{ 'phi2 $a $i}.
114 interpretation "phi2" 'phi2 a i = (phi a i).
115 notation < "Ď a" non associative with precedence 90 for @{ 'phi1 $a }.
116 interpretation "phi2" 'phi1 a = (phi a).
118 ndefinition caxs : uAx.
119 @; ##[ @ nat (Îť_.unit); #a; #_; napply { x | Ď a x = O } ##| #_; @; ##]
123 alias id "S" = "cic:/matita/ng/topology/igft/S.fix(0,0,1)".
124 unification hint 0 â ;
126 (* -------------- *) â˘
129 naxiom h : nat â nat.
131 alias symbol "eq" = "leibnitz's equality".
132 alias symbol "eq" = "setoid1 eq".
133 alias symbol "covers" = "covers".
134 alias symbol "eq" = "leibnitz's equality".
135 naxiom Ph : âx.h x = O \liff x â â
.
138 âA:Ax.âU,V.U â V â V â U â âa:A.a â U â a â V.
139 #A; #U; #V; #a; #H1; #H2; #E; nelim E;
140 ##[ #b; #Hb; @; nauto;
141 ##| #b; #i; #H3; #H4; @2 i; #c; #Hc; nauto; ##]
144 ntheorem th_ch3: ÂŹâa:caxs.âx.Ď a x = h x.
146 ncut (a â { x | x â â
}); ##[
147 napply (replace_char ⌠{ x | h x = O }); ##[ ##1,2: #x; ncases (Ph x);
148 (* nauto; *) #H1; #H2; #H3; nauto; (* ??? *) ##]
149 napply (replace_char ⌠{ x | Ď a x = O }); ##[##1,2: #x; nrewrite > (H x);
150 (* nauto; *) #E; napply E; ##]
151 napply (axiom_cond ⌠a one); ##] #H1;
152 ncut (a â â
); ##[ napply (transitivity ⌠H1); #x; nauto; ##] #H2;
153 nlapply (col2_4 âŚH2); #H3;
154 ncut (a â đ a one); ##[
155 nnormalize; ncases (Ph a); nrewrite > (H a); nauto; ##] #H4;