15647

1 
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)


2 

17566

3 
theory HOL4Real imports HOL4Base begin

14516

4 


5 
;setup_theory realax


6 


7 
lemma HREAL_RDISTRIB: "ALL x y z.


8 
hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)"


9 
by (import realax HREAL_RDISTRIB)


10 


11 
lemma HREAL_EQ_ADDL: "ALL x y. x ~= hreal_add x y"


12 
by (import realax HREAL_EQ_ADDL)


13 


14 
lemma HREAL_EQ_LADD: "ALL x y z. (hreal_add x y = hreal_add x z) = (y = z)"


15 
by (import realax HREAL_EQ_LADD)


16 


17 
lemma HREAL_LT_REFL: "ALL x. ~ hreal_lt x x"


18 
by (import realax HREAL_LT_REFL)


19 


20 
lemma HREAL_LT_ADDL: "ALL x y. hreal_lt x (hreal_add x y)"


21 
by (import realax HREAL_LT_ADDL)


22 


23 
lemma HREAL_LT_NE: "ALL x y. hreal_lt x y > x ~= y"


24 
by (import realax HREAL_LT_NE)


25 


26 
lemma HREAL_LT_ADDR: "ALL x y. ~ hreal_lt (hreal_add x y) x"


27 
by (import realax HREAL_LT_ADDR)


28 


29 
lemma HREAL_LT_GT: "ALL x y. hreal_lt x y > ~ hreal_lt y x"


30 
by (import realax HREAL_LT_GT)


31 


32 
lemma HREAL_LT_ADD2: "ALL x1 x2 y1 y2.


33 
hreal_lt x1 y1 & hreal_lt x2 y2 >


34 
hreal_lt (hreal_add x1 x2) (hreal_add y1 y2)"


35 
by (import realax HREAL_LT_ADD2)


36 


37 
lemma HREAL_LT_LADD: "ALL x y z. hreal_lt (hreal_add x y) (hreal_add x z) = hreal_lt y z"


38 
by (import realax HREAL_LT_LADD)


39 


40 
constdefs


41 
treal_0 :: "hreal * hreal"


42 
"treal_0 == (hreal_1, hreal_1)"


43 


44 
lemma treal_0: "treal_0 = (hreal_1, hreal_1)"


45 
by (import realax treal_0)


46 


47 
constdefs


48 
treal_1 :: "hreal * hreal"


49 
"treal_1 == (hreal_add hreal_1 hreal_1, hreal_1)"


50 


51 
lemma treal_1: "treal_1 = (hreal_add hreal_1 hreal_1, hreal_1)"


52 
by (import realax treal_1)


53 


54 
constdefs


55 
treal_neg :: "hreal * hreal => hreal * hreal"


56 
"treal_neg == %(x, y). (y, x)"


57 


58 
lemma treal_neg: "ALL x y. treal_neg (x, y) = (y, x)"


59 
by (import realax treal_neg)


60 


61 
constdefs


62 
treal_add :: "hreal * hreal => hreal * hreal => hreal * hreal"


63 
"treal_add == %(x1, y1) (x2, y2). (hreal_add x1 x2, hreal_add y1 y2)"


64 


65 
lemma treal_add: "ALL x1 y1 x2 y2.


66 
treal_add (x1, y1) (x2, y2) = (hreal_add x1 x2, hreal_add y1 y2)"


67 
by (import realax treal_add)


68 


69 
constdefs


70 
treal_mul :: "hreal * hreal => hreal * hreal => hreal * hreal"


71 
"treal_mul ==


72 
%(x1, y1) (x2, y2).


73 
(hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2),


74 
hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))"


75 


76 
lemma treal_mul: "ALL x1 y1 x2 y2.


77 
treal_mul (x1, y1) (x2, y2) =


78 
(hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2),


79 
hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))"


80 
by (import realax treal_mul)


81 


82 
constdefs


83 
treal_lt :: "hreal * hreal => hreal * hreal => bool"


84 
"treal_lt == %(x1, y1) (x2, y2). hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)"


85 


86 
lemma treal_lt: "ALL x1 y1 x2 y2.


87 
treal_lt (x1, y1) (x2, y2) = hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)"


88 
by (import realax treal_lt)


89 


90 
constdefs


91 
treal_inv :: "hreal * hreal => hreal * hreal"


92 
"treal_inv ==


93 
%(x, y).


94 
if x = y then treal_0


95 
else if hreal_lt y x


96 
then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1)


97 
else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1)"


98 


99 
lemma treal_inv: "ALL x y.


100 
treal_inv (x, y) =


101 
(if x = y then treal_0


102 
else if hreal_lt y x


103 
then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1)


104 
else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1))"


105 
by (import realax treal_inv)


106 


107 
constdefs


108 
treal_eq :: "hreal * hreal => hreal * hreal => bool"


109 
"treal_eq == %(x1, y1) (x2, y2). hreal_add x1 y2 = hreal_add x2 y1"


110 


111 
lemma treal_eq: "ALL x1 y1 x2 y2.


112 
treal_eq (x1, y1) (x2, y2) = (hreal_add x1 y2 = hreal_add x2 y1)"


113 
by (import realax treal_eq)


114 


115 
lemma TREAL_EQ_REFL: "ALL x. treal_eq x x"


116 
by (import realax TREAL_EQ_REFL)


117 


118 
lemma TREAL_EQ_SYM: "ALL x y. treal_eq x y = treal_eq y x"


119 
by (import realax TREAL_EQ_SYM)


120 


121 
lemma TREAL_EQ_TRANS: "ALL x y z. treal_eq x y & treal_eq y z > treal_eq x z"


122 
by (import realax TREAL_EQ_TRANS)


123 


124 
lemma TREAL_EQ_EQUIV: "ALL p q. treal_eq p q = (treal_eq p = treal_eq q)"


125 
by (import realax TREAL_EQ_EQUIV)


126 


127 
lemma TREAL_EQ_AP: "ALL p q. p = q > treal_eq p q"


128 
by (import realax TREAL_EQ_AP)


129 


130 
lemma TREAL_10: "~ treal_eq treal_1 treal_0"


131 
by (import realax TREAL_10)


132 


133 
lemma TREAL_ADD_SYM: "ALL x y. treal_add x y = treal_add y x"


134 
by (import realax TREAL_ADD_SYM)


135 


136 
lemma TREAL_MUL_SYM: "ALL x y. treal_mul x y = treal_mul y x"


137 
by (import realax TREAL_MUL_SYM)


138 


139 
lemma TREAL_ADD_ASSOC: "ALL x y z. treal_add x (treal_add y z) = treal_add (treal_add x y) z"


140 
by (import realax TREAL_ADD_ASSOC)


141 


142 
lemma TREAL_MUL_ASSOC: "ALL x y z. treal_mul x (treal_mul y z) = treal_mul (treal_mul x y) z"


143 
by (import realax TREAL_MUL_ASSOC)


144 


145 
lemma TREAL_LDISTRIB: "ALL x y z.


146 
treal_mul x (treal_add y z) = treal_add (treal_mul x y) (treal_mul x z)"


147 
by (import realax TREAL_LDISTRIB)


148 


149 
lemma TREAL_ADD_LID: "ALL x. treal_eq (treal_add treal_0 x) x"


150 
by (import realax TREAL_ADD_LID)


151 


152 
lemma TREAL_MUL_LID: "ALL x. treal_eq (treal_mul treal_1 x) x"


153 
by (import realax TREAL_MUL_LID)


154 


155 
lemma TREAL_ADD_LINV: "ALL x. treal_eq (treal_add (treal_neg x) x) treal_0"


156 
by (import realax TREAL_ADD_LINV)


157 


158 
lemma TREAL_INV_0: "treal_eq (treal_inv treal_0) treal_0"


159 
by (import realax TREAL_INV_0)


160 


161 
lemma TREAL_MUL_LINV: "ALL x. ~ treal_eq x treal_0 > treal_eq (treal_mul (treal_inv x) x) treal_1"


162 
by (import realax TREAL_MUL_LINV)


163 


164 
lemma TREAL_LT_TOTAL: "ALL x y. treal_eq x y  treal_lt x y  treal_lt y x"


165 
by (import realax TREAL_LT_TOTAL)


166 


167 
lemma TREAL_LT_REFL: "ALL x. ~ treal_lt x x"


168 
by (import realax TREAL_LT_REFL)


169 


170 
lemma TREAL_LT_TRANS: "ALL x y z. treal_lt x y & treal_lt y z > treal_lt x z"


171 
by (import realax TREAL_LT_TRANS)


172 


173 
lemma TREAL_LT_ADD: "ALL x y z. treal_lt y z > treal_lt (treal_add x y) (treal_add x z)"


174 
by (import realax TREAL_LT_ADD)


175 


176 
lemma TREAL_LT_MUL: "ALL x y.


177 
treal_lt treal_0 x & treal_lt treal_0 y >


178 
treal_lt treal_0 (treal_mul x y)"


179 
by (import realax TREAL_LT_MUL)


180 


181 
constdefs


182 
treal_of_hreal :: "hreal => hreal * hreal"


183 
"treal_of_hreal == %x. (hreal_add x hreal_1, hreal_1)"


184 


185 
lemma treal_of_hreal: "ALL x. treal_of_hreal x = (hreal_add x hreal_1, hreal_1)"


186 
by (import realax treal_of_hreal)


187 


188 
constdefs


189 
hreal_of_treal :: "hreal * hreal => hreal"


190 
"hreal_of_treal == %(x, y). SOME d. x = hreal_add y d"


191 


192 
lemma hreal_of_treal: "ALL x y. hreal_of_treal (x, y) = (SOME d. x = hreal_add y d)"


193 
by (import realax hreal_of_treal)


194 


195 
lemma TREAL_BIJ: "(ALL h. hreal_of_treal (treal_of_hreal h) = h) &


196 
(ALL r. treal_lt treal_0 r = treal_eq (treal_of_hreal (hreal_of_treal r)) r)"


197 
by (import realax TREAL_BIJ)


198 


199 
lemma TREAL_ISO: "ALL h i. hreal_lt h i > treal_lt (treal_of_hreal h) (treal_of_hreal i)"


200 
by (import realax TREAL_ISO)


201 


202 
lemma TREAL_BIJ_WELLDEF: "ALL h i. treal_eq h i > hreal_of_treal h = hreal_of_treal i"


203 
by (import realax TREAL_BIJ_WELLDEF)


204 


205 
lemma TREAL_NEG_WELLDEF: "ALL x1 x2. treal_eq x1 x2 > treal_eq (treal_neg x1) (treal_neg x2)"


206 
by (import realax TREAL_NEG_WELLDEF)


207 


208 
lemma TREAL_ADD_WELLDEFR: "ALL x1 x2 y. treal_eq x1 x2 > treal_eq (treal_add x1 y) (treal_add x2 y)"


209 
by (import realax TREAL_ADD_WELLDEFR)


210 


211 
lemma TREAL_ADD_WELLDEF: "ALL x1 x2 y1 y2.


212 
treal_eq x1 x2 & treal_eq y1 y2 >


213 
treal_eq (treal_add x1 y1) (treal_add x2 y2)"


214 
by (import realax TREAL_ADD_WELLDEF)


215 


216 
lemma TREAL_MUL_WELLDEFR: "ALL x1 x2 y. treal_eq x1 x2 > treal_eq (treal_mul x1 y) (treal_mul x2 y)"


217 
by (import realax TREAL_MUL_WELLDEFR)


218 


219 
lemma TREAL_MUL_WELLDEF: "ALL x1 x2 y1 y2.


220 
treal_eq x1 x2 & treal_eq y1 y2 >


221 
treal_eq (treal_mul x1 y1) (treal_mul x2 y2)"


222 
by (import realax TREAL_MUL_WELLDEF)


223 


224 
lemma TREAL_LT_WELLDEFR: "ALL x1 x2 y. treal_eq x1 x2 > treal_lt x1 y = treal_lt x2 y"


225 
by (import realax TREAL_LT_WELLDEFR)


226 


227 
lemma TREAL_LT_WELLDEFL: "ALL x y1 y2. treal_eq y1 y2 > treal_lt x y1 = treal_lt x y2"


228 
by (import realax TREAL_LT_WELLDEFL)


229 


230 
lemma TREAL_LT_WELLDEF: "ALL x1 x2 y1 y2.


231 
treal_eq x1 x2 & treal_eq y1 y2 > treal_lt x1 y1 = treal_lt x2 y2"


232 
by (import realax TREAL_LT_WELLDEF)


233 


234 
lemma TREAL_INV_WELLDEF: "ALL x1 x2. treal_eq x1 x2 > treal_eq (treal_inv x1) (treal_inv x2)"


235 
by (import realax TREAL_INV_WELLDEF)


236 


237 
;end_setup


238 


239 
;setup_theory real


240 


241 
lemma REAL_0: "(0::real) = (0::real)"


242 
by (import real REAL_0)


243 


244 
lemma REAL_1: "(1::real) = (1::real)"


245 
by (import real REAL_1)


246 


247 
lemma REAL_ADD_LID_UNIQ: "ALL (x::real) y::real. (x + y = y) = (x = (0::real))"


248 
by (import real REAL_ADD_LID_UNIQ)


249 


250 
lemma REAL_ADD_RID_UNIQ: "ALL (x::real) y::real. (x + y = x) = (y = (0::real))"


251 
by (import real REAL_ADD_RID_UNIQ)


252 


253 
lemma REAL_LNEG_UNIQ: "ALL (x::real) y::real. (x + y = (0::real)) = (x =  y)"


254 
by (import real REAL_LNEG_UNIQ)


255 


256 
lemma REAL_LT_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y < x)"


257 
by (import real REAL_LT_ANTISYM)


258 


259 
lemma REAL_LTE_TOTAL: "ALL (x::real) y::real. x < y  y <= x"


260 
by (import real REAL_LTE_TOTAL)


261 


262 
lemma REAL_LET_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y <= x)"


263 
by (import real REAL_LET_ANTISYM)


264 


265 
lemma REAL_LTE_ANTSYM: "ALL (x::real) y::real. ~ (x <= y & y < x)"


266 
by (import real REAL_LTE_ANTSYM)


267 


268 
lemma REAL_LT_NEGTOTAL: "ALL x::real. x = (0::real)  (0::real) < x  (0::real) <  x"


269 
by (import real REAL_LT_NEGTOTAL)


270 


271 
lemma REAL_LE_NEGTOTAL: "ALL x::real. (0::real) <= x  (0::real) <=  x"


272 
by (import real REAL_LE_NEGTOTAL)


273 


274 
lemma REAL_LT_ADDNEG: "ALL (x::real) (y::real) z::real. (y < x +  z) = (y + z < x)"


275 
by (import real REAL_LT_ADDNEG)


276 


277 
lemma REAL_LT_ADDNEG2: "ALL (x::real) (y::real) z::real. (x +  y < z) = (x < z + y)"


278 
by (import real REAL_LT_ADDNEG2)


279 


280 
lemma REAL_LT_ADD1: "ALL (x::real) y::real. x <= y > x < y + (1::real)"


281 
by (import real REAL_LT_ADD1)


282 

14796

283 
lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x  y) = x"


284 
by (import real REAL_SUB_ADD2)


285 

15647

286 
lemma REAL_SUB_LT: "ALL (x::real) y::real. ((0::real) < x  y) = (y < x)"


287 
by (import real REAL_SUB_LT)


288 


289 
lemma REAL_SUB_LE: "ALL (x::real) y::real. ((0::real) <= x  y) = (y <= x)"


290 
by (import real REAL_SUB_LE)


291 

14796

292 
lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y  x = y"


293 
by (import real REAL_ADD_SUB)

14516

294 


295 
lemma REAL_NEG_EQ: "ALL (x::real) y::real. ( x = y) = (x =  y)"


296 
by (import real REAL_NEG_EQ)


297 


298 
lemma REAL_NEG_MINUS1: "ALL x::real.  x =  (1::real) * x"


299 
by (import real REAL_NEG_MINUS1)


300 


301 
lemma REAL_LT_LMUL_0: "ALL (x::real) y::real.


302 
(0::real) < x > ((0::real) < x * y) = ((0::real) < y)"


303 
by (import real REAL_LT_LMUL_0)


304 


305 
lemma REAL_LT_RMUL_0: "ALL (x::real) y::real.


306 
(0::real) < y > ((0::real) < x * y) = ((0::real) < x)"


307 
by (import real REAL_LT_RMUL_0)


308 


309 
lemma REAL_LT_LMUL: "ALL (x::real) (y::real) z::real. (0::real) < x > (x * y < x * z) = (y < z)"


310 
by (import real REAL_LT_LMUL)


311 


312 
lemma REAL_LINV_UNIQ: "ALL (x::real) y::real. x * y = (1::real) > x = inverse y"


313 
by (import real REAL_LINV_UNIQ)


314 

15647

315 
lemma REAL_LE_INV: "ALL x>=0::real. (0::real) <= inverse x"

14516

316 
by (import real REAL_LE_INV)


317 


318 
lemma REAL_LE_ADDR: "ALL (x::real) y::real. (x <= x + y) = ((0::real) <= y)"


319 
by (import real REAL_LE_ADDR)


320 


321 
lemma REAL_LE_ADDL: "ALL (x::real) y::real. (y <= x + y) = ((0::real) <= x)"


322 
by (import real REAL_LE_ADDL)


323 


324 
lemma REAL_LT_ADDR: "ALL (x::real) y::real. (x < x + y) = ((0::real) < y)"


325 
by (import real REAL_LT_ADDR)


326 


327 
lemma REAL_LT_ADDL: "ALL (x::real) y::real. (y < x + y) = ((0::real) < x)"


328 
by (import real REAL_LT_ADDL)


329 


330 
lemma REAL_LT_NZ: "ALL n::nat. (real n ~= (0::real)) = ((0::real) < real n)"


331 
by (import real REAL_LT_NZ)


332 


333 
lemma REAL_NZ_IMP_LT: "ALL n::nat. n ~= (0::nat) > (0::real) < real n"


334 
by (import real REAL_NZ_IMP_LT)


335 


336 
lemma REAL_LT_RDIV_0: "ALL (y::real) z::real.


337 
(0::real) < z > ((0::real) < y / z) = ((0::real) < y)"


338 
by (import real REAL_LT_RDIV_0)


339 


340 
lemma REAL_LT_RDIV: "ALL (x::real) (y::real) z::real. (0::real) < z > (x / z < y / z) = (x < y)"


341 
by (import real REAL_LT_RDIV)


342 


343 
lemma REAL_LT_FRACTION_0: "ALL (n::nat) d::real.


344 
n ~= (0::nat) > ((0::real) < d / real n) = ((0::real) < d)"


345 
by (import real REAL_LT_FRACTION_0)


346 


347 
lemma REAL_LT_MULTIPLE: "ALL (x::nat) xa::real.


348 
(1::nat) < x > (xa < real x * xa) = ((0::real) < xa)"


349 
by (import real REAL_LT_MULTIPLE)


350 


351 
lemma REAL_LT_FRACTION: "ALL (n::nat) d::real. (1::nat) < n > (d / real n < d) = ((0::real) < d)"


352 
by (import real REAL_LT_FRACTION)


353 


354 
lemma REAL_LT_HALF2: "ALL d::real. (d / (2::real) < d) = ((0::real) < d)"


355 
by (import real REAL_LT_HALF2)


356 


357 
lemma REAL_DIV_LMUL: "ALL (x::real) y::real. y ~= (0::real) > y * (x / y) = x"


358 
by (import real REAL_DIV_LMUL)


359 


360 
lemma REAL_DIV_RMUL: "ALL (x::real) y::real. y ~= (0::real) > x / y * y = x"


361 
by (import real REAL_DIV_RMUL)


362 

15647

363 
lemma REAL_DOWN: "ALL x>0::real. EX xa>0::real. xa < x"

14516

364 
by (import real REAL_DOWN)


365 


366 
lemma REAL_SUB_SUB: "ALL (x::real) y::real. x  y  x =  y"


367 
by (import real REAL_SUB_SUB)


368 


369 
lemma REAL_ADD2_SUB2: "ALL (a::real) (b::real) (c::real) d::real. a + b  (c + d) = a  c + (b  d)"


370 
by (import real REAL_ADD2_SUB2)


371 


372 
lemma REAL_SUB_LNEG: "ALL (x::real) y::real.  x  y =  (x + y)"


373 
by (import real REAL_SUB_LNEG)


374 


375 
lemma REAL_SUB_NEG2: "ALL (x::real) y::real.  x   y = y  x"


376 
by (import real REAL_SUB_NEG2)


377 


378 
lemma REAL_SUB_TRIANGLE: "ALL (a::real) (b::real) c::real. a  b + (b  c) = a  c"


379 
by (import real REAL_SUB_TRIANGLE)


380 


381 
lemma REAL_INV_MUL: "ALL (x::real) y::real.


382 
x ~= (0::real) & y ~= (0::real) >


383 
inverse (x * y) = inverse x * inverse y"


384 
by (import real REAL_INV_MUL)


385 


386 
lemma REAL_SUB_INV2: "ALL (x::real) y::real.


387 
x ~= (0::real) & y ~= (0::real) >


388 
inverse x  inverse y = (y  x) / (x * y)"


389 
by (import real REAL_SUB_INV2)


390 


391 
lemma REAL_SUB_SUB2: "ALL (x::real) y::real. x  (x  y) = y"


392 
by (import real REAL_SUB_SUB2)


393 


394 
lemma REAL_ADD_SUB2: "ALL (x::real) y::real. x  (x + y) =  y"


395 
by (import real REAL_ADD_SUB2)


396 


397 
lemma REAL_LE_MUL2: "ALL (x1::real) (x2::real) (y1::real) y2::real.


398 
(0::real) <= x1 & (0::real) <= y1 & x1 <= x2 & y1 <= y2 >


399 
x1 * y1 <= x2 * y2"


400 
by (import real REAL_LE_MUL2)


401 


402 
lemma REAL_LE_DIV: "ALL (x::real) xa::real.


403 
(0::real) <= x & (0::real) <= xa > (0::real) <= x / xa"


404 
by (import real REAL_LE_DIV)


405 


406 
lemma REAL_LT_1: "ALL (x::real) y::real. (0::real) <= x & x < y > x / y < (1::real)"


407 
by (import real REAL_LT_1)


408 

15647

409 
lemma REAL_POS_NZ: "ALL x>0::real. x ~= (0::real)"

14516

410 
by (import real REAL_POS_NZ)


411 


412 
lemma REAL_EQ_LMUL_IMP: "ALL (x::real) (xa::real) xb::real.


413 
x ~= (0::real) & x * xa = x * xb > xa = xb"


414 
by (import real REAL_EQ_LMUL_IMP)


415 


416 
lemma REAL_FACT_NZ: "ALL n. real (FACT n) ~= 0"


417 
by (import real REAL_FACT_NZ)


418 


419 
lemma REAL_DIFFSQ: "ALL (x::real) y::real. (x + y) * (x  y) = x * x  y * y"


420 
by (import real REAL_DIFFSQ)


421 


422 
lemma REAL_POASQ: "ALL x::real. ((0::real) < x * x) = (x ~= (0::real))"


423 
by (import real REAL_POASQ)


424 


425 
lemma REAL_SUMSQ: "ALL (x::real) y::real.


426 
(x * x + y * y = (0::real)) = (x = (0::real) & y = (0::real))"


427 
by (import real REAL_SUMSQ)


428 

17188

429 
lemma REAL_DIV_MUL2: "ALL (x::real) z::real.


430 
x ~= (0::real) & z ~= (0::real) >


431 
(ALL y::real. y / z = x * y / (x * z))"


432 
by (import real REAL_DIV_MUL2)


433 

14516

434 
lemma REAL_MIDDLE1: "ALL (a::real) b::real. a <= b > a <= (a + b) / (2::real)"


435 
by (import real REAL_MIDDLE1)


436 


437 
lemma REAL_MIDDLE2: "ALL (a::real) b::real. a <= b > (a + b) / (2::real) <= b"


438 
by (import real REAL_MIDDLE2)


439 


440 
lemma ABS_LT_MUL2: "ALL (w::real) (x::real) (y::real) z::real.


441 
abs w < y & abs x < z > abs (w * x) < y * z"


442 
by (import real ABS_LT_MUL2)


443 


444 
lemma ABS_REFL: "ALL x::real. (abs x = x) = ((0::real) <= x)"


445 
by (import real ABS_REFL)


446 


447 
lemma ABS_BETWEEN: "ALL (x::real) (y::real) d::real.


448 
((0::real) < d & x  d < y & y < x + d) = (abs (y  x) < d)"


449 
by (import real ABS_BETWEEN)


450 


451 
lemma ABS_BOUND: "ALL (x::real) (y::real) d::real. abs (x  y) < d > y < x + d"


452 
by (import real ABS_BOUND)


453 


454 
lemma ABS_STILLNZ: "ALL (x::real) y::real. abs (x  y) < abs y > x ~= (0::real)"


455 
by (import real ABS_STILLNZ)


456 


457 
lemma ABS_CASES: "ALL x::real. x = (0::real)  (0::real) < abs x"


458 
by (import real ABS_CASES)


459 


460 
lemma ABS_BETWEEN1: "ALL (x::real) (y::real) z::real. x < z & abs (y  x) < z  x > y < z"


461 
by (import real ABS_BETWEEN1)


462 


463 
lemma ABS_SIGN: "ALL (x::real) y::real. abs (x  y) < y > (0::real) < x"


464 
by (import real ABS_SIGN)


465 


466 
lemma ABS_SIGN2: "ALL (x::real) y::real. abs (x  y) <  y > x < (0::real)"


467 
by (import real ABS_SIGN2)


468 


469 
lemma ABS_CIRCLE: "ALL (x::real) (y::real) h::real.


470 
abs h < abs y  abs x > abs (x + h) < abs y"


471 
by (import real ABS_CIRCLE)


472 


473 
lemma ABS_BETWEEN2: "ALL (x0::real) (x::real) (y0::real) y::real.


474 
x0 < y0 &


475 
abs (x  x0) < (y0  x0) / (2::real) &


476 
abs (y  y0) < (y0  x0) / (2::real) >


477 
x < y"


478 
by (import real ABS_BETWEEN2)


479 

15647

480 
lemma POW_PLUS1: "ALL e>0. ALL n. 1 + real n * e <= (1 + e) ^ n"

14516

481 
by (import real POW_PLUS1)


482 


483 
lemma POW_M1: "ALL n::nat. abs (( (1::real)) ^ n) = (1::real)"


484 
by (import real POW_M1)


485 

15647

486 
lemma REAL_LE1_POW2: "ALL x>=1::real. (1::real) <= x ^ 2"

14516

487 
by (import real REAL_LE1_POW2)


488 

15647

489 
lemma REAL_LT1_POW2: "ALL x>1::real. (1::real) < x ^ 2"

14516

490 
by (import real REAL_LT1_POW2)


491 


492 
lemma POW_POS_LT: "ALL (x::real) n::nat. (0::real) < x > (0::real) < x ^ Suc n"


493 
by (import real POW_POS_LT)


494 


495 
lemma POW_LT: "ALL (n::nat) (x::real) y::real.


496 
(0::real) <= x & x < y > x ^ Suc n < y ^ Suc n"


497 
by (import real POW_LT)


498 


499 
lemma POW_ZERO_EQ: "ALL (n::nat) x::real. (x ^ Suc n = (0::real)) = (x = (0::real))"


500 
by (import real POW_ZERO_EQ)


501 


502 
lemma REAL_POW_LT2: "ALL (n::nat) (x::real) y::real.


503 
n ~= (0::nat) & (0::real) <= x & x < y > x ^ n < y ^ n"


504 
by (import real REAL_POW_LT2)


505 

17188

506 
lemma REAL_POW_MONO_LT: "ALL (m::nat) (n::nat) x::real. (1::real) < x & m < n > x ^ m < x ^ n"


507 
by (import real REAL_POW_MONO_LT)


508 

14516

509 
lemma REAL_SUP_SOMEPOS: "ALL P::real => bool.


510 
(EX x::real. P x & (0::real) < x) &


511 
(EX z::real. ALL x::real. P x > x < z) >


512 
(EX s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))"


513 
by (import real REAL_SUP_SOMEPOS)


514 


515 
lemma SUP_LEMMA1: "ALL (P::real => bool) (s::real) d::real.


516 
(ALL y::real. (EX x::real. P (x + d) & y < x) = (y < s)) >


517 
(ALL y::real. (EX x::real. P x & y < x) = (y < s + d))"


518 
by (import real SUP_LEMMA1)


519 


520 
lemma SUP_LEMMA2: "ALL P::real => bool.


521 
Ex P > (EX (d::real) x::real. P (x + d) & (0::real) < x)"


522 
by (import real SUP_LEMMA2)


523 


524 
lemma SUP_LEMMA3: "ALL d::real.


525 
(EX z::real. ALL x::real. (P::real => bool) x > x < z) >


526 
(EX x::real. ALL xa::real. P (xa + d) > xa < x)"


527 
by (import real SUP_LEMMA3)


528 


529 
lemma REAL_SUP_EXISTS: "ALL P::real => bool.


530 
Ex P & (EX z::real. ALL x::real. P x > x < z) >


531 
(EX x::real. ALL y::real. (EX x::real. P x & y < x) = (y < x))"


532 
by (import real REAL_SUP_EXISTS)


533 


534 
constdefs


535 
sup :: "(real => bool) => real"


536 
"sup == %P. SOME s. ALL y. (EX x. P x & y < x) = (y < s)"


537 


538 
lemma sup: "ALL P. sup P = (SOME s. ALL y. (EX x. P x & y < x) = (y < s))"


539 
by (import real sup)


540 


541 
lemma REAL_SUP: "ALL P.


542 
Ex P & (EX z. ALL x. P x > x < z) >


543 
(ALL y. (EX x. P x & y < x) = (y < sup P))"


544 
by (import real REAL_SUP)


545 


546 
lemma REAL_SUP_UBOUND: "ALL P. Ex P & (EX z. ALL x. P x > x < z) > (ALL y. P y > y <= sup P)"


547 
by (import real REAL_SUP_UBOUND)


548 


549 
lemma SETOK_LE_LT: "ALL P::real => bool.


550 
(Ex P & (EX z::real. ALL x::real. P x > x <= z)) =


551 
(Ex P & (EX z::real. ALL x::real. P x > x < z))"


552 
by (import real SETOK_LE_LT)


553 


554 
lemma REAL_SUP_LE: "ALL P.


555 
Ex P & (EX z. ALL x. P x > x <= z) >


556 
(ALL y. (EX x. P x & y < x) = (y < sup P))"


557 
by (import real REAL_SUP_LE)


558 


559 
lemma REAL_SUP_UBOUND_LE: "ALL P. Ex P & (EX z. ALL x. P x > x <= z) > (ALL y. P y > y <= sup P)"


560 
by (import real REAL_SUP_UBOUND_LE)


561 

15647

562 
lemma REAL_ARCH_LEAST: "ALL y>0. ALL x>=0. EX n. real n * y <= x & x < real (Suc n) * y"

14516

563 
by (import real REAL_ARCH_LEAST)


564 


565 
consts


566 
sumc :: "nat => nat => (nat => real) => real"


567 


568 
specification (sumc) sumc: "(ALL n f. sumc n 0 f = 0) &


569 
(ALL n m f. sumc n (Suc m) f = sumc n m f + f (n + m))"


570 
by (import real sumc)


571 

14694

572 
consts

14516

573 
sum :: "nat * nat => (nat => real) => real"

14694

574 


575 
defs

15647

576 
sum_def: "(op ==::(nat * nat => (nat => real) => real)


577 
=> (nat * nat => (nat => real) => real) => prop)


578 
(real.sum::nat * nat => (nat => real) => real)


579 
((split::(nat => nat => (nat => real) => real)


580 
=> nat * nat => (nat => real) => real)


581 
(sumc::nat => nat => (nat => real) => real))"

14516

582 


583 
lemma SUM_DEF: "ALL m n f. real.sum (m, n) f = sumc m n f"


584 
by (import real SUM_DEF)


585 


586 
lemma sum: "ALL x xa xb.


587 
real.sum (xa, 0) x = 0 &


588 
real.sum (xa, Suc xb) x = real.sum (xa, xb) x + x (xa + xb)"


589 
by (import real sum)


590 


591 
lemma SUM_TWO: "ALL f n p. real.sum (0, n) f + real.sum (n, p) f = real.sum (0, n + p) f"


592 
by (import real SUM_TWO)


593 


594 
lemma SUM_DIFF: "ALL f m n. real.sum (m, n) f = real.sum (0, m + n) f  real.sum (0, m) f"


595 
by (import real SUM_DIFF)


596 


597 
lemma ABS_SUM: "ALL f m n. abs (real.sum (m, n) f) <= real.sum (m, n) (%n. abs (f n))"


598 
by (import real ABS_SUM)


599 


600 
lemma SUM_LE: "ALL f g m n.


601 
(ALL r. m <= r & r < n + m > f r <= g r) >


602 
real.sum (m, n) f <= real.sum (m, n) g"


603 
by (import real SUM_LE)


604 


605 
lemma SUM_EQ: "ALL f g m n.


606 
(ALL r. m <= r & r < n + m > f r = g r) >


607 
real.sum (m, n) f = real.sum (m, n) g"


608 
by (import real SUM_EQ)


609 


610 
lemma SUM_POS: "ALL f. (ALL n. 0 <= f n) > (ALL m n. 0 <= real.sum (m, n) f)"


611 
by (import real SUM_POS)


612 


613 
lemma SUM_POS_GEN: "ALL f m. (ALL n. m <= n > 0 <= f n) > (ALL n. 0 <= real.sum (m, n) f)"


614 
by (import real SUM_POS_GEN)


615 


616 
lemma SUM_ABS: "ALL f m x.


617 
abs (real.sum (m, x) (%m. abs (f m))) = real.sum (m, x) (%m. abs (f m))"


618 
by (import real SUM_ABS)


619 


620 
lemma SUM_ABS_LE: "ALL f m n. abs (real.sum (m, n) f) <= real.sum (m, n) (%n. abs (f n))"


621 
by (import real SUM_ABS_LE)


622 


623 
lemma SUM_ZERO: "ALL f N.


624 
(ALL n. N <= n > f n = 0) >


625 
(ALL m n. N <= m > real.sum (m, n) f = 0)"


626 
by (import real SUM_ZERO)


627 


628 
lemma SUM_ADD: "ALL f g m n.


629 
real.sum (m, n) (%n. f n + g n) = real.sum (m, n) f + real.sum (m, n) g"


630 
by (import real SUM_ADD)


631 


632 
lemma SUM_CMUL: "ALL f c m n. real.sum (m, n) (%n. c * f n) = c * real.sum (m, n) f"


633 
by (import real SUM_CMUL)


634 


635 
lemma SUM_NEG: "ALL f n d. real.sum (n, d) (%n.  f n) =  real.sum (n, d) f"


636 
by (import real SUM_NEG)


637 


638 
lemma SUM_SUB: "ALL f g m n.


639 
real.sum (m, n) (%x. f x  g x) = real.sum (m, n) f  real.sum (m, n) g"


640 
by (import real SUM_SUB)


641 


642 
lemma SUM_SUBST: "ALL f g m n.


643 
(ALL p. m <= p & p < m + n > f p = g p) >


644 
real.sum (m, n) f = real.sum (m, n) g"


645 
by (import real SUM_SUBST)


646 


647 
lemma SUM_NSUB: "ALL n f c. real.sum (0, n) f  real n * c = real.sum (0, n) (%p. f p  c)"


648 
by (import real SUM_NSUB)


649 


650 
lemma SUM_BOUND: "ALL f k m n.


651 
(ALL p. m <= p & p < m + n > f p <= k) >


652 
real.sum (m, n) f <= real n * k"


653 
by (import real SUM_BOUND)


654 


655 
lemma SUM_GROUP: "ALL n k f.


656 
real.sum (0, n) (%m. real.sum (m * k, k) f) = real.sum (0, n * k) f"


657 
by (import real SUM_GROUP)


658 


659 
lemma SUM_1: "ALL f n. real.sum (n, 1) f = f n"


660 
by (import real SUM_1)


661 


662 
lemma SUM_2: "ALL f n. real.sum (n, 2) f = f n + f (n + 1)"


663 
by (import real SUM_2)


664 


665 
lemma SUM_OFFSET: "ALL f n k.


666 
real.sum (0, n) (%m. f (m + k)) =


667 
real.sum (0, n + k) f  real.sum (0, k) f"


668 
by (import real SUM_OFFSET)


669 


670 
lemma SUM_REINDEX: "ALL f m k n. real.sum (m + k, n) f = real.sum (m, n) (%r. f (r + k))"


671 
by (import real SUM_REINDEX)


672 


673 
lemma SUM_0: "ALL m n. real.sum (m, n) (%r. 0) = 0"


674 
by (import real SUM_0)


675 

14847

676 
lemma SUM_PERMUTE_0: "(All::(nat => bool) => bool)


677 
(%n::nat.


678 
(All::((nat => nat) => bool) => bool)


679 
(%p::nat => nat.


680 
(op >::bool => bool => bool)


681 
((All::(nat => bool) => bool)


682 
(%y::nat.


683 
(op >::bool => bool => bool)


684 
((op <::nat => nat => bool) y n)


685 
((Ex1::(nat => bool) => bool)


686 
(%x::nat.


687 
(op &::bool => bool => bool)


688 
((op <::nat => nat => bool) x n)


689 
((op =::nat => nat => bool) (p x) y)))))


690 
((All::((nat => real) => bool) => bool)


691 
(%f::nat => real.


692 
(op =::real => real => bool)


693 
((real.sum::nat * nat => (nat => real) => real)


694 
((Pair::nat => nat => nat * nat) (0::nat) n)


695 
(%n::nat. f (p n)))


696 
((real.sum::nat * nat => (nat => real) => real)


697 
((Pair::nat => nat => nat * nat) (0::nat) n) f)))))"

14516

698 
by (import real SUM_PERMUTE_0)


699 


700 
lemma SUM_CANCEL: "ALL f n d. real.sum (n, d) (%n. f (Suc n)  f n) = f (n + d)  f n"


701 
by (import real SUM_CANCEL)


702 


703 
lemma REAL_EQ_RDIV_EQ: "ALL (x::real) (xa::real) xb::real.


704 
(0::real) < xb > (x = xa / xb) = (x * xb = xa)"


705 
by (import real REAL_EQ_RDIV_EQ)


706 


707 
lemma REAL_EQ_LDIV_EQ: "ALL (x::real) (xa::real) xb::real.


708 
(0::real) < xb > (x / xb = xa) = (x = xa * xb)"


709 
by (import real REAL_EQ_LDIV_EQ)


710 


711 
;end_setup


712 


713 
;setup_theory topology


714 


715 
constdefs


716 
re_Union :: "(('a => bool) => bool) => 'a => bool"


717 
"re_Union == %P x. EX s. P s & s x"


718 


719 
lemma re_Union: "ALL P. re_Union P = (%x. EX s. P s & s x)"


720 
by (import topology re_Union)


721 


722 
constdefs


723 
re_union :: "('a => bool) => ('a => bool) => 'a => bool"


724 
"re_union == %P Q x. P x  Q x"


725 


726 
lemma re_union: "ALL P Q. re_union P Q = (%x. P x  Q x)"


727 
by (import topology re_union)


728 


729 
constdefs


730 
re_intersect :: "('a => bool) => ('a => bool) => 'a => bool"


731 
"re_intersect == %P Q x. P x & Q x"


732 


733 
lemma re_intersect: "ALL P Q. re_intersect P Q = (%x. P x & Q x)"


734 
by (import topology re_intersect)


735 


736 
constdefs


737 
re_null :: "'a => bool"


738 
"re_null == %x. False"


739 


740 
lemma re_null: "re_null = (%x. False)"


741 
by (import topology re_null)


742 


743 
constdefs


744 
re_universe :: "'a => bool"


745 
"re_universe == %x. True"


746 


747 
lemma re_universe: "re_universe = (%x. True)"


748 
by (import topology re_universe)


749 


750 
constdefs


751 
re_subset :: "('a => bool) => ('a => bool) => bool"


752 
"re_subset == %P Q. ALL x. P x > Q x"


753 


754 
lemma re_subset: "ALL P Q. re_subset P Q = (ALL x. P x > Q x)"


755 
by (import topology re_subset)


756 


757 
constdefs


758 
re_compl :: "('a => bool) => 'a => bool"


759 
"re_compl == %P x. ~ P x"


760 


761 
lemma re_compl: "ALL P. re_compl P = (%x. ~ P x)"


762 
by (import topology re_compl)


763 


764 
lemma SUBSET_REFL: "ALL P. re_subset P P"


765 
by (import topology SUBSET_REFL)


766 


767 
lemma COMPL_MEM: "ALL P x. P x = (~ re_compl P x)"


768 
by (import topology COMPL_MEM)


769 


770 
lemma SUBSET_ANTISYM: "ALL P Q. (re_subset P Q & re_subset Q P) = (P = Q)"


771 
by (import topology SUBSET_ANTISYM)


772 


773 
lemma SUBSET_TRANS: "ALL P Q R. re_subset P Q & re_subset Q R > re_subset P R"


774 
by (import topology SUBSET_TRANS)


775 


776 
constdefs


777 
istopology :: "(('a => bool) => bool) => bool"


778 
"istopology ==


779 
%L. L re_null &


780 
L re_universe &


781 
(ALL a b. L a & L b > L (re_intersect a b)) &


782 
(ALL P. re_subset P L > L (re_Union P))"


783 


784 
lemma istopology: "ALL L.


785 
istopology L =


786 
(L re_null &


787 
L re_universe &


788 
(ALL a b. L a & L b > L (re_intersect a b)) &


789 
(ALL P. re_subset P L > L (re_Union P)))"


790 
by (import topology istopology)


791 


792 
typedef (open) ('a) topology = "(Collect::((('a => bool) => bool) => bool) => (('a => bool) => bool) set)


793 
(istopology::(('a => bool) => bool) => bool)"


794 
by (rule typedef_helper,import topology topology_TY_DEF)


795 


796 
lemmas topology_TY_DEF = typedef_hol2hol4 [OF type_definition_topology]


797 


798 
consts


799 
topology :: "(('a => bool) => bool) => 'a topology"


800 
"open" :: "'a topology => ('a => bool) => bool"


801 


802 
specification ("open" topology) topology_tybij: "(ALL a::'a topology. topology (open a) = a) &


803 
(ALL r::('a => bool) => bool. istopology r = (open (topology r) = r))"


804 
by (import topology topology_tybij)


805 


806 
lemma TOPOLOGY: "ALL L.


807 
open L re_null &


808 
open L re_universe &


809 
(ALL a b. open L a & open L b > open L (re_intersect a b)) &


810 
(ALL P. re_subset P (open L) > open L (re_Union P))"


811 
by (import topology TOPOLOGY)


812 


813 
lemma TOPOLOGY_UNION: "ALL x xa. re_subset xa (open x) > open x (re_Union xa)"


814 
by (import topology TOPOLOGY_UNION)


815 


816 
constdefs


817 
neigh :: "'a topology => ('a => bool) * 'a => bool"


818 
"neigh == %top (N, x). EX P. open top P & re_subset P N & P x"


819 


820 
lemma neigh: "ALL top N x. neigh top (N, x) = (EX P. open top P & re_subset P N & P x)"


821 
by (import topology neigh)


822 


823 
lemma OPEN_OWN_NEIGH: "ALL S' top x. open top S' & S' x > neigh top (S', x)"


824 
by (import topology OPEN_OWN_NEIGH)


825 


826 
lemma OPEN_UNOPEN: "ALL S' top. open top S' = (re_Union (%P. open top P & re_subset P S') = S')"


827 
by (import topology OPEN_UNOPEN)


828 


829 
lemma OPEN_SUBOPEN: "ALL S' top.


830 
open top S' = (ALL x. S' x > (EX P. P x & open top P & re_subset P S'))"


831 
by (import topology OPEN_SUBOPEN)


832 


833 
lemma OPEN_NEIGH: "ALL S' top.


834 
open top S' = (ALL x. S' x > (EX N. neigh top (N, x) & re_subset N S'))"


835 
by (import topology OPEN_NEIGH)


836 


837 
constdefs


838 
closed :: "'a topology => ('a => bool) => bool"


839 
"closed == %L S'. open L (re_compl S')"


840 


841 
lemma closed: "ALL L S'. closed L S' = open L (re_compl S')"


842 
by (import topology closed)


843 


844 
constdefs


845 
limpt :: "'a topology => 'a => ('a => bool) => bool"


846 
"limpt == %top x S'. ALL N. neigh top (N, x) > (EX y. x ~= y & S' y & N y)"


847 


848 
lemma limpt: "ALL top x S'.


849 
limpt top x S' =


850 
(ALL N. neigh top (N, x) > (EX y. x ~= y & S' y & N y))"


851 
by (import topology limpt)


852 


853 
lemma CLOSED_LIMPT: "ALL top S'. closed top S' = (ALL x. limpt top x S' > S' x)"


854 
by (import topology CLOSED_LIMPT)


855 


856 
constdefs


857 
ismet :: "('a * 'a => real) => bool"


858 
"ismet ==


859 
%m. (ALL x y. (m (x, y) = 0) = (x = y)) &


860 
(ALL x y z. m (y, z) <= m (x, y) + m (x, z))"


861 


862 
lemma ismet: "ALL m.


863 
ismet m =


864 
((ALL x y. (m (x, y) = 0) = (x = y)) &


865 
(ALL x y z. m (y, z) <= m (x, y) + m (x, z)))"


866 
by (import topology ismet)


867 


868 
typedef (open) ('a) metric = "(Collect::(('a * 'a => real) => bool) => ('a * 'a => real) set)


869 
(ismet::('a * 'a => real) => bool)"


870 
by (rule typedef_helper,import topology metric_TY_DEF)


871 


872 
lemmas metric_TY_DEF = typedef_hol2hol4 [OF type_definition_metric]


873 


874 
consts


875 
metric :: "('a * 'a => real) => 'a metric"


876 
dist :: "'a metric => 'a * 'a => real"


877 


878 
specification (dist metric) metric_tybij: "(ALL a::'a metric. metric (dist a) = a) &


879 
(ALL r::'a * 'a => real. ismet r = (dist (metric r) = r))"


880 
by (import topology metric_tybij)


881 


882 
lemma METRIC_ISMET: "ALL m. ismet (dist m)"


883 
by (import topology METRIC_ISMET)


884 


885 
lemma METRIC_ZERO: "ALL m x y. (dist m (x, y) = 0) = (x = y)"


886 
by (import topology METRIC_ZERO)


887 


888 
lemma METRIC_SAME: "ALL m x. dist m (x, x) = 0"


889 
by (import topology METRIC_SAME)


890 


891 
lemma METRIC_POS: "ALL m x y. 0 <= dist m (x, y)"


892 
by (import topology METRIC_POS)


893 


894 
lemma METRIC_SYM: "ALL m x y. dist m (x, y) = dist m (y, x)"


895 
by (import topology METRIC_SYM)


896 


897 
lemma METRIC_TRIANGLE: "ALL m x y z. dist m (x, z) <= dist m (x, y) + dist m (y, z)"


898 
by (import topology METRIC_TRIANGLE)


899 


900 
lemma METRIC_NZ: "ALL m x y. x ~= y > 0 < dist m (x, y)"


901 
by (import topology METRIC_NZ)


902 


903 
constdefs


904 
mtop :: "'a metric => 'a topology"


905 
"mtop ==


906 
%m. topology

15647

907 
(%S'. ALL x. S' x > (EX e>0. ALL y. dist m (x, y) < e > S' y))"

14516

908 


909 
lemma mtop: "ALL m.


910 
mtop m =


911 
topology

15647

912 
(%S'. ALL x. S' x > (EX e>0. ALL y. dist m (x, y) < e > S' y))"

14516

913 
by (import topology mtop)


914 


915 
lemma mtop_istopology: "ALL m.


916 
istopology

15647

917 
(%S'. ALL x. S' x > (EX e>0. ALL y. dist m (x, y) < e > S' y))"

14516

918 
by (import topology mtop_istopology)


919 


920 
lemma MTOP_OPEN: "ALL S' x.


921 
open (mtop x) S' =

15647

922 
(ALL xa. S' xa > (EX e>0. ALL y. dist x (xa, y) < e > S' y))"

14516

923 
by (import topology MTOP_OPEN)


924 


925 
constdefs


926 
B :: "'a metric => 'a * real => 'a => bool"


927 
"B == %m (x, e) y. dist m (x, y) < e"


928 


929 
lemma ball: "ALL m x e. B m (x, e) = (%y. dist m (x, y) < e)"


930 
by (import topology ball)


931 


932 
lemma BALL_OPEN: "ALL m x e. 0 < e > open (mtop m) (B m (x, e))"


933 
by (import topology BALL_OPEN)


934 


935 
lemma BALL_NEIGH: "ALL m x e. 0 < e > neigh (mtop m) (B m (x, e), x)"


936 
by (import topology BALL_NEIGH)


937 


938 
lemma MTOP_LIMPT: "ALL m x S'.

15647

939 
limpt (mtop m) x S' = (ALL e>0. EX y. x ~= y & S' y & dist m (x, y) < e)"

14516

940 
by (import topology MTOP_LIMPT)


941 


942 
lemma ISMET_R1: "ismet (%(x, y). abs (y  x))"


943 
by (import topology ISMET_R1)


944 


945 
constdefs


946 
mr1 :: "real metric"


947 
"mr1 == metric (%(x, y). abs (y  x))"


948 


949 
lemma mr1: "mr1 = metric (%(x, y). abs (y  x))"


950 
by (import topology mr1)


951 


952 
lemma MR1_DEF: "ALL x y. dist mr1 (x, y) = abs (y  x)"


953 
by (import topology MR1_DEF)


954 


955 
lemma MR1_ADD: "ALL x d. dist mr1 (x, x + d) = abs d"


956 
by (import topology MR1_ADD)


957 


958 
lemma MR1_SUB: "ALL x d. dist mr1 (x, x  d) = abs d"


959 
by (import topology MR1_SUB)


960 


961 
lemma MR1_ADD_POS: "ALL x d. 0 <= d > dist mr1 (x, x + d) = d"


962 
by (import topology MR1_ADD_POS)


963 


964 
lemma MR1_SUB_LE: "ALL x d. 0 <= d > dist mr1 (x, x  d) = d"


965 
by (import topology MR1_SUB_LE)


966 


967 
lemma MR1_ADD_LT: "ALL x d. 0 < d > dist mr1 (x, x + d) = d"


968 
by (import topology MR1_ADD_LT)


969 


970 
lemma MR1_SUB_LT: "ALL x d. 0 < d > dist mr1 (x, x  d) = d"


971 
by (import topology MR1_SUB_LT)


972 


973 
lemma MR1_BETWEEN1: "ALL x y z. x < z & dist mr1 (x, y) < z  x > y < z"


974 
by (import topology MR1_BETWEEN1)


975 


976 
lemma MR1_LIMPT: "ALL x. limpt (mtop mr1) x re_universe"


977 
by (import topology MR1_LIMPT)


978 


979 
;end_setup


980 


981 
;setup_theory nets


982 


983 
constdefs


984 
dorder :: "('a => 'a => bool) => bool"


985 
"dorder ==


986 
%g. ALL x y.


987 
g x x & g y y > (EX z. g z z & (ALL w. g w z > g w x & g w y))"


988 


989 
lemma dorder: "ALL g.


990 
dorder g =


991 
(ALL x y.


992 
g x x & g y y > (EX z. g z z & (ALL w. g w z > g w x & g w y)))"


993 
by (import nets dorder)


994 


995 
constdefs


996 
tends :: "('b => 'a) => 'a => 'a topology * ('b => 'b => bool) => bool"


997 
"tends ==


998 
%(s::'b => 'a) (l::'a) (top::'a topology, g::'b => 'b => bool).


999 
ALL N::'a => bool.


1000 
neigh top (N, l) >


1001 
(EX n::'b. g n n & (ALL m::'b. g m n > N (s m)))"


1002 


1003 
lemma tends: "ALL (s::'b => 'a) (l::'a) (top::'a topology) g::'b => 'b => bool.


1004 
tends s l (top, g) =


1005 
(ALL N::'a => bool.


1006 
neigh top (N, l) >


1007 
(EX n::'b. g n n & (ALL m::'b. g m n > N (s m))))"


1008 
by (import nets tends)


1009 


1010 
constdefs


1011 
bounded :: "'a metric * ('b => 'b => bool) => ('b => 'a) => bool"


1012 
"bounded ==


1013 
%(m, g) f. EX k x N. g N N & (ALL n. g n N > dist m (f n, x) < k)"


1014 


1015 
lemma bounded: "ALL m g f.


1016 
bounded (m, g) f =


1017 
(EX k x N. g N N & (ALL n. g n N > dist m (f n, x) < k))"


1018 
by (import nets bounded)


1019 


1020 
constdefs


1021 
tendsto :: "'a metric * 'a => 'a => 'a => bool"


1022 
"tendsto == %(m, x) y z. 0 < dist m (x, y) & dist m (x, y) <= dist m (x, z)"


1023 


1024 
lemma tendsto: "ALL m x y z.


1025 
tendsto (m, x) y z = (0 < dist m (x, y) & dist m (x, y) <= dist m (x, z))"


1026 
by (import nets tendsto)


1027 


1028 
lemma DORDER_LEMMA: "ALL g.


1029 
dorder g >


1030 
(ALL P Q.


1031 
(EX n. g n n & (ALL m. g m n > P m)) &


1032 
(EX n. g n n & (ALL m. g m n > Q m)) >


1033 
(EX n. g n n & (ALL m. g m n > P m & Q m)))"


1034 
by (import nets DORDER_LEMMA)


1035 


1036 
lemma DORDER_NGE: "dorder nat_ge"


1037 
by (import nets DORDER_NGE)


1038 


1039 
lemma DORDER_TENDSTO: "ALL m x. dorder (tendsto (m, x))"


1040 
by (import nets DORDER_TENDSTO)


1041 


1042 
lemma MTOP_TENDS: "ALL d g x x0.


1043 
tends x x0 (mtop d, g) =

15647

1044 
(ALL e>0. EX n. g n n & (ALL m. g m n > dist d (x m, x0) < e))"

14516

1045 
by (import nets MTOP_TENDS)


1046 


1047 
lemma MTOP_TENDS_UNIQ: "ALL (g::'b => 'b => bool) d::'a metric.


1048 
dorder g >


1049 
tends (x::'b => 'a) (x0::'a) (mtop d, g) &


1050 
tends x (x1::'a) (mtop d, g) >


1051 
x0 = x1"


1052 
by (import nets MTOP_TENDS_UNIQ)


1053 


1054 
lemma SEQ_TENDS: "ALL d x x0.


1055 
tends x x0 (mtop d, nat_ge) =

15647

1056 
(ALL xa>0. EX xb. ALL xc. xb <= xc > dist d (x xc, x0) < xa)"

14516

1057 
by (import nets SEQ_TENDS)


1058 


1059 
lemma LIM_TENDS: "ALL m1 m2 f x0 y0.


1060 
limpt (mtop m1) x0 re_universe >


1061 
tends f y0 (mtop m2, tendsto (m1, x0)) =

15647

1062 
(ALL e>0.


1063 
EX d>0.


1064 
ALL x.


1065 
0 < dist m1 (x, x0) & dist m1 (x, x0) <= d >


1066 
dist m2 (f x, y0) < e)"

14516

1067 
by (import nets LIM_TENDS)


1068 


1069 
lemma LIM_TENDS2: "ALL m1 m2 f x0 y0.


1070 
limpt (mtop m1) x0 re_universe >


1071 
tends f y0 (mtop m2, tendsto (m1, x0)) =

15647

1072 
(ALL e>0.


1073 
EX d>0.


1074 
ALL x.


1075 
0 < dist m1 (x, x0) & dist m1 (x, x0) < d >


1076 
dist m2 (f x, y0) < e)"

14516

1077 
by (import nets LIM_TENDS2)


1078 


1079 
lemma MR1_BOUNDED: "ALL g f.


1080 
bounded (mr1, g) f = (EX k N. g N N & (ALL n. g n N > abs (f n) < k))"


1081 
by (import nets MR1_BOUNDED)


1082 


1083 
lemma NET_NULL: "ALL g x x0. tends x x0 (mtop mr1, g) = tends (%n. x n  x0) 0 (mtop mr1, g)"


1084 
by (import nets NET_NULL)


1085 


1086 
lemma NET_CONV_BOUNDED: "ALL g x x0. tends x x0 (mtop mr1, g) > bounded (mr1, g) x"


1087 
by (import nets NET_CONV_BOUNDED)


1088 


1089 
lemma NET_CONV_NZ: "ALL g x x0.


1090 
tends x x0 (mtop mr1, g) & x0 ~= 0 >


1091 
(EX N. g N N & (ALL n. g n N > x n ~= 0))"


1092 
by (import nets NET_CONV_NZ)


1093 


1094 
lemma NET_CONV_IBOUNDED: "ALL g x x0.


1095 
tends x x0 (mtop mr1, g) & x0 ~= 0 >


1096 
bounded (mr1, g) (%n. inverse (x n))"


1097 
by (import nets NET_CONV_IBOUNDED)


1098 


1099 
lemma NET_NULL_ADD: "ALL g.


1100 
dorder g >


1101 
(ALL x y.


1102 
tends x 0 (mtop mr1, g) & tends y 0 (mtop mr1, g) >


1103 
tends (%n. x n + y n) 0 (mtop mr1, g))"


1104 
by (import nets NET_NULL_ADD)


1105 


1106 
lemma NET_NULL_MUL: "ALL g.


1107 
dorder g >


1108 
(ALL x y.


1109 
bounded (mr1, g) x & tends y 0 (mtop mr1, g) >


1110 
tends (%n. x n * y n) 0 (mtop mr1, g))"


1111 
by (import nets NET_NULL_MUL)


1112 


1113 
lemma NET_NULL_CMUL: "ALL g k x. tends x 0 (mtop mr1, g) > tends (%n. k * x n) 0 (mtop mr1, g)"


1114 
by (import nets NET_NULL_CMUL)


1115 


1116 
lemma NET_ADD: "ALL g.


1117 
dorder g >


1118 
(ALL x x0 y y0.


1119 
tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) >


1120 
tends (%n. x n + y n) (x0 + y0) (mtop mr1, g))"


1121 
by (import nets NET_ADD)


1122 


1123 
lemma NET_NEG: "ALL g.


1124 
dorder g >


1125 
(ALL x x0.


1126 
tends x x0 (mtop mr1, g) = tends (%n.  x n) ( x0) (mtop mr1, g))"


1127 
by (import nets NET_NEG)


1128 


1129 
lemma NET_SUB: "ALL g.


1130 
dorder g >


1131 
(ALL x x0 y y0.


1132 
tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) >


1133 
tends (%xa. x xa  y xa) (x0  y0) (mtop mr1, g))"


1134 
by (import nets NET_SUB)


1135 


1136 
lemma NET_MUL: "ALL g.


1137 
dorder g >


1138 
(ALL x y x0 y0.


1139 
tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) >


1140 
tends (%n. x n * y n) (x0 * y0) (mtop mr1, g))"


1141 
by (import nets NET_MUL)


1142 


1143 
lemma NET_INV: "ALL g.


1144 
dorder g >


1145 
(ALL x x0.


1146 
tends x x0 (mtop mr1, g) & x0 ~= 0 >


1147 
tends (%n. inverse (x n)) (inverse x0) (mtop mr1, g))"


1148 
by (import nets NET_INV)


1149 


1150 
lemma NET_DIV: "ALL g.


1151 
dorder g >


1152 
(ALL x x0 y y0.


1153 
tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) & y0 ~= 0 >


1154 
tends (%xa. x xa / y xa) (x0 / y0) (mtop mr1, g))"


1155 
by (import nets NET_DIV)


1156 


1157 
lemma NET_ABS: "ALL g x x0.


1158 
tends x x0 (mtop mr1, g) > tends (%n. abs (x n)) (abs x0) (mtop mr1, g)"


1159 
by (import nets NET_ABS)


1160 


1161 
lemma NET_LE: "ALL g.


1162 
dorder g >


1163 
(ALL x x0 y y0.


1164 
tends x x0 (mtop mr1, g) &


1165 
tends y y0 (mtop mr1, g) &


1166 
(EX N. g N N & (ALL n. g n N > x n <= y n)) >


1167 
x0 <= y0)"


1168 
by (import nets NET_LE)


1169 


1170 
;end_setup


1171 


1172 
;setup_theory seq


1173 

14694

1174 
consts

14516

1175 
">" :: "(nat => real) => real => bool" (">")

14694

1176 


1177 
defs


1178 
">_def": "> == %x x0. tends x x0 (mtop mr1, nat_ge)"

14516

1179 


1180 
lemma tends_num_real: "ALL x x0. > x x0 = tends x x0 (mtop mr1, nat_ge)"


1181 
by (import seq tends_num_real)


1182 


1183 
lemma SEQ: "(All::((nat => real) => bool) => bool)


1184 
(%x::nat => real.


1185 
(All::(real => bool) => bool)


1186 
(%x0::real.


1187 
(op =::bool => bool => bool)


1188 
((>::(nat => real) => real => bool) x x0)


1189 
((All::(real => bool) => bool)


1190 
(%e::real.


1191 
(op >::bool => bool => bool)


1192 
((op <::real => real => bool) (0::real) e)


1193 
((Ex::(nat => bool) => bool)


1194 
(%N::nat.


1195 
(All::(nat => bool) => bool)


1196 
(%n::nat.


1197 
(op >::bool => bool => bool)


1198 
((op <=::nat => nat => bool) N n)


1199 
((op <::real => real => bool)


1200 
((abs::real => real)


1201 
((op ::real => real => real) (x n) x0))


1202 
e))))))))"


1203 
by (import seq SEQ)


1204 


1205 
lemma SEQ_CONST: "ALL k. > (%x. k) k"


1206 
by (import seq SEQ_CONST)


1207 


1208 
lemma SEQ_ADD: "(All::((nat => real) => bool) => bool)


1209 
(%x::nat => real.


1210 
(All::(real => bool) => bool)


1211 
(%x0::real.


1212 
(All::((nat => real) => bool) => bool)


1213 
(%y::nat => real.


1214 
(All::(real => bool) => bool)


1215 
(%y0::real.


1216 
(op >::bool => bool => bool)


1217 
((op &::bool => bool => bool)


1218 
((>::(nat => real) => real => bool) x x0)


1219 
((>::(nat => real) => real => bool) y y0))


1220 
((>::(nat => real) => real => bool)


1221 
(%n::nat. (op +::real => real => real) (x n) (y n))


1222 
((op +::real => real => real) x0 y0))))))"


1223 
by (import seq SEQ_ADD)


1224 


1225 
lemma SEQ_MUL: "(All::((nat => real) => bool) => bool)


1226 
(%x::nat => real.


1227 
(All::(real => bool) => bool)


1228 
(%x0::real.


1229 
(All::((nat => real) => bool) => bool)


1230 
(%y::nat => real.


1231 
(All::(real => bool) => bool)


1232 
(%y0::real.


1233 
(op >::bool => bool => bool)


1234 
((op &::bool => bool => bool)


1235 
((>::(nat => real) => real => bool) x x0)


1236 
((>::(nat => real) => real => bool) y y0))


1237 
((>::(nat => real) => real => bool)


1238 
(%n::nat. (op *::real => real => real) (x n) (y n))


1239 
((op *::real => real => real) x0 y0))))))"


1240 
by (import seq SEQ_MUL)


1241 


1242 
lemma SEQ_NEG: "ALL x x0. > x x0 = > (%n.  x n) ( x0)"


1243 
by (import seq SEQ_NEG)


1244 


1245 
lemma SEQ_INV: "(All::((nat => real) => bool) => bool)


1246 
(%x::nat => real.


1247 
(All::(real => bool) => bool)


1248 
(%x0::real.


1249 
(op >::bool => bool => bool)


1250 
((op &::bool => bool => bool)


1251 
((>::(nat => real) => real => bool) x x0)


1252 
((Not::bool => bool)


1253 
((op =::real => real => bool) x0 (0::real))))


1254 
((>::(nat => real) => real => bool)


1255 
(%n::nat. (inverse::real => real) (x n))


1256 
((inverse::real => real) x0))))"


1257 
by (import seq SEQ_INV)


1258 


1259 
lemma SEQ_SUB: "(All::((nat => real) => bool) => bool)


1260 
(%x::nat => real.


1261 
(All::(real => bool) => bool)


1262 
(%x0::real.


1263 
(All::((nat => real) => bool) => bool)


1264 
(%y::nat => real.


1265 
(All::(real => bool) => bool)


1266 
(%y0::real.


1267 
(op >::bool => bool => bool)


1268 
((op &::bool => bool => bool)


1269 
((>::(nat => real) => real => bool) x x0)


1270 
((>::(nat => real) => real => bool) y y0))


1271 
((>::(nat => real) => real => bool)


1272 
(%n::nat. (op ::real => real => real) (x n) (y n))


1273 
((op ::real => real => real) x0 y0))))))"


1274 
by (import seq SEQ_SUB)


1275 


1276 
lemma SEQ_DIV: "(All::((nat => real) => bool) => bool)


1277 
(%x::nat => real.


1278 
(All::(real => bool) => bool)


1279 
(%x0::real.


1280 
(All::((nat => real) => bool) => bool)


1281 
(%y::nat => real.


1282 
(All::(real => bool) => bool)


1283 
(%y0::real.


1284 
(op >::bool => bool => bool)


1285 
((op &::bool => bool => bool)


1286 
((>::(nat => real) => real => bool) x x0)


1287 
((op &::bool => bool => bool)


1288 
((>::(nat => real) => real => bool) y y0)


1289 
((Not::bool => bool)


1290 
((op =::real => real => bool) y0 (0::real)))))


1291 
((>::(nat => real) => real => bool)


1292 
(%n::nat. (op /::real => real => real) (x n) (y n))


1293 
((op /::real => real => real) x0 y0))))))"


1294 
by (import seq SEQ_DIV)


1295 


1296 
lemma SEQ_UNIQ: "(All::((nat => real) => bool) => bool)


1297 
(%x::nat => real.


1298 
(All::(real => bool) => bool)


1299 
(%x1::real.


1300 
(All::(real => bool) => bool)


1301 
(%x2::real.


1302 
(op >::bool => bool => bool)


1303 
((op &::bool => bool => bool)


1304 
((>::(nat => real) => real => bool) x x1)


1305 
((>::(nat => real) => real => bool) x x2))


1306 
((op =::real => real => bool) x1 x2))))"


1307 
by (import seq SEQ_UNIQ)


1308 


1309 
constdefs


1310 
convergent :: "(nat => real) => bool"


1311 
"convergent == %f. Ex (> f)"


1312 


1313 
lemma convergent: "ALL f. convergent f = Ex (> f)"


1314 
by (import seq convergent)


1315 


1316 
constdefs


1317 
cauchy :: "(nat => real) => bool"


1318 
"(op ==::((nat => real) => bool) => ((nat => real) => bool) => prop)


1319 
(cauchy::(nat => real) => bool)


1320 
(%f::nat => real.


1321 
(All::(real => bool) => bool)


1322 
(%e::real.


1323 
(op >::bool => bool => bool)


1324 
((op <::real => real => bool) (0::real) e)


1325 
((Ex::(nat => bool) => bool)


1326 
(%N::nat.


1327 
(All::(nat => bool) => bool)


1328 
(%m::nat.


1329 
(All::(nat => bool) => bool)


1330 
(%n::nat.


1331 
(op >::bool => bool => bool)


1332 
((op &::bool => bool => bool)


1333 
((op <=::nat => nat => bool) N m)


1334 
((op <=::nat => nat => bool) N n))


1335 
((op <::real => real => bool)


1336 
((abs::real => real)


1337 
((op ::real => real => real) (f m) (f n)))


1338 
e)))))))"


1339 


1340 
lemma cauchy: "(All::((nat => real) => bool) => bool)


1341 
(%f::nat => real.


1342 
(op =::bool => bool => bool) ((cauchy::(nat => real) => bool) f)


1343 
((All::(real => bool) => bool)


1344 
(%e::real.


1345 
(op >::bool => bool => bool)


1346 
((op <::real => real => bool) (0::real) e)


1347 
((Ex::(nat => bool) => bool)


1348 
(%N::nat.


1349 
(All::(nat => bool) => bool)


1350 
(%m::nat.


1351 
(All::(nat => bool) => bool)


1352 
(%n::nat.


1353 
(op >::bool => bool => bool)


1354 
((op &::bool => bool => bool)


1355 
((op <=::nat => nat => bool) N m)


1356 
((op <=::nat => nat => bool) N n))


1357 
((op <::real => real => bool)


1358 
((abs::real => real)


1359 
((op ::real => real => real) (f m)


1360 
(f n)))


1361 
e))))))))"


1362 
by (import seq cauchy)


1363 


1364 
constdefs


1365 
lim :: "(nat => real) => real"


1366 
"lim == %f. Eps (> f)"


1367 


1368 
lemma lim: "ALL f. lim f = Eps (> f)"


1369 
by (import seq lim)


1370 


1371 
lemma SEQ_LIM: "ALL f. convergent f = > f (lim f)"


1372 
by (import seq SEQ_LIM)


1373 


1374 
constdefs


1375 
subseq :: "(nat => nat) => bool"


1376 
"(op ==::((nat => nat) => bool) => ((nat => nat) => bool) => prop)


1377 
(subseq::(nat => nat) => bool)


1378 
(%f::nat => nat.


1379 
(All::(nat => bool) => bool)


1380 
(%m::nat.


1381 
(All::(nat => bool) => bool)


1382 
(%n::nat.


1383 
(op >::bool => bool => bool)


1384 
((op <::nat => nat => bool) m n)


1385 
((op <::nat => nat => bool) (f m) (f n)))))"


1386 


1387 
lemma subseq: "(All::((nat => nat) => bool) => bool)


1388 
(%f::nat => nat.


1389 
(op =::bool => bool => bool) ((subseq::(nat => nat) => bool) f)


1390 
((All::(nat => bool) => bool)


1391 
(%m::nat.


1392 
(All::(nat => bool) => bool)


1393 
(%n::nat.


1394 
(op >::bool => bool => bool)


1395 
((op <::nat => nat => bool) m n)


1396 
((op <::nat => nat => bool) (f m) (f n))))))"


1397 
by (import seq subseq)


1398 


1399 
lemma SUBSEQ_SUC: "ALL f. subseq f = (ALL n. f n < f (Suc n))"


1400 
by (import seq SUBSEQ_SUC)


1401 

14694

1402 
consts

14516

1403 
mono :: "(nat => real) => bool"

14694

1404 


1405 
defs


1406 
mono_def: "(op ==::((nat => real) => bool) => ((nat => real) => bool) => prop)

14516

1407 
(seq.mono::(nat => real) => bool)


1408 
(%f::nat => real.


1409 
(op ::bool => bool => bool)


1410 
((All::(nat => bool) => bool)


1411 
(%m::nat.


1412 
(All::(nat => bool) => bool)


1413 
(%n::nat.


1414 
(op >::bool => bool => bool)


1415 
((op <=::nat => nat => bool) m n)


1416 
((op <=::real => real => bool) (f m) (f n)))))


1417 
((All::(nat => bool) => bool)


1418 
(%m::nat.


1419 
(All::(nat => bool) => bool)


1420 
(%n::nat.


1421 
(op >::bool => bool => bool)


1422 
((op <=::nat => nat => bool) m n)


1423 
((op <=::real => real => bool) (f n) (f m))))))"


1424 


1425 
lemma mono: "(All::((nat => real) => bool) => bool)


1426 
(%f::nat => real.


1427 
(op =::bool => bool => bool) ((seq.mono::(nat => real) => bool) f)


1428 
((op ::bool => bool => bool)


1429 
((All::(nat => bool) => bool)


1430 
(%m::nat.


1431 
(All::(nat => bool) => bool)


1432 
(%n::nat.


1433 
(op >::bool => bool => bool)


1434 
((op <=::nat => nat => bool) m n)


1435 
((op <=::real => real => bool) (f m) (f n)))))


1436 
((All::(nat => bool) => bool)


1437 
(%m::nat.


1438 
(All::(nat => bool) => bool)


1439 
(%n::nat.


1440 
(op >::bool => bool => bool)


1441 
((op <=::nat => nat => bool) m n)


1442 
((op <=::real => real => bool) (f n) (f m)))))))"


1443 
by (import seq mono)


1444 


1445 
lemma MONO_SUC: "ALL f. seq.mono f = ((ALL x. f x <= f (Suc x))  (ALL n. f (Suc n) <= f n))"


1446 
by (import seq MONO_SUC)


1447 

14847

1448 
lemma MAX_LEMMA: "(All::((nat => real) => bool) => bool)


1449 
(%s::nat => real.


1450 
(All::(nat => bool) => bool)


1451 
(%N::nat.


1452 
(Ex::(real => bool) => bool)


1453 
(%k::real.


1454 
(All::(nat => bool) => bool)


1455 
(%n::nat.


1456 
(op >::bool => bool => bool)


1457 
((op <::nat => nat => bool) n N)


1458 
((op <::real => real => bool)


1459 
((abs::real => real) (s n)) k)))))"

14516

1460 
by (import seq MAX_LEMMA)


1461 


1462 
lemma SEQ_BOUNDED: "ALL s. bounded (mr1, nat_ge) s = (EX k. ALL n. abs (s n) < k)"


1463 
by (import seq SEQ_BOUNDED)


1464 


1465 
lemma SEQ_BOUNDED_2: "(All::((nat => real) => bool) => bool)


1466 
(%f::nat => real.


1467 
(All::(real => bool) => bool)


1468 
(%k::real.


1469 
(All::(real => bool) => bool)


1470 
(%k'::real.


1471 
(op >::bool => bool => bool)


1472 
((All::(nat => bool) => bool)


1473 
(%n::nat.


1474 
(op &::bool => bool => bool)


1475 
((op <=::real => real => bool) k (f n))

