Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Bounding Boxes for Compact Sets in $\calE^2$

**by****Czeslaw Bylinski, and****Piotr Rudnicki**- Received July 29, 1997
- MML identifier: PSCOMP_1

- [ Mizar article, MML identifier index ]

environ vocabulary AMI_1, FREEALG, HAHNBAN, COMPTS_1, BOOLE, FINSET_1, ZFMISC_1, SETFAM_1, FUNCT_1, RELAT_1, ABSVALUE, ARYTM_1, SEQ_1, SEQ_2, ORDINAL2, LATTICES, ARYTM_3, SEQ_4, PRE_TOPC, RCOMP_1, FUNCOP_1, PRALG_1, SUBSET_1, NEWTON, INT_1, REALSET1, LIMFUNC1, PCOMPS_1, EUCLID, TOPREAL1, FUNCT_5, MCART_1, PSCOMP_1, ARYTM, MEMBERED; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SETFAM_1, FINSET_1, STRUCT_0, FINSOP_1, ABSVALUE, REAL_1, NAT_1, INT_1, MEMBERED, RELAT_1, FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, AMI_1, SEQ_4, RCOMP_1, LIMFUNC1, PRE_TOPC, TOPS_2, COMPTS_1, PCOMPS_1, EUCLID, TOPREAL1; constructors REAL_1, TOPS_2, NAT_1, INT_1, FINSOP_1, ABSVALUE, SEQ_2, SEQ_4, AMI_1, RCOMP_1, COMPTS_1, LIMFUNC1, TOPREAL1, SEQM_3, TSP_1, PCOMPS_1, XCMPLX_0, XREAL_0, MEMBERED, RELSET_1, PARTFUN1, XBOOLE_0; clusters NUMBERS, SUBSET_1, STRUCT_0, PRE_TOPC, RCOMP_1, SEQM_3, EUCLID, PCOMPS_1, FUNCT_1, XREAL_0, RELSET_1, SEQ_1, REAL_1, SETFAM_1, INT_1, XBOOLE_0, SEQ_2, NAT_1, MEMBERED, RELAT_1, FUNCT_2, ZFMISC_1, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries definition let X be set; redefine attr X is with_non-empty_elements means :: PSCOMP_1:def 1 not 0 in X; synonym X is without_zero; antonym X is with_zero; end; definition cluster REAL -> with_zero; cluster NAT -> with_zero; end; definition cluster non empty without_zero set; cluster non empty with_zero set; end; definition cluster non empty without_zero Subset of REAL; cluster non empty with_zero Subset of REAL; end; theorem :: PSCOMP_1:1 for F being set st F is non empty with_non-empty_elements c=-linear holds F is centered; definition let F be set; cluster non empty with_non-empty_elements c=-linear -> centered Subset-Family of F; end; definition let A, B be set, f be Function of A, B; redefine func rng f -> Subset of B; end; definition let X, Y be non empty set, f be Function of X, Y; :: see WAYBEL_2 cluster f.:X -> non empty; end; definition let X, Y be set, f be Function of X, Y; func "f -> Function of bool Y, bool X means :: PSCOMP_1:def 2 :: see FUNCT_3:def 2 for y being Subset of Y holds it.y = f"y; end; theorem :: PSCOMP_1:2 for X, Y, x being set, S being Subset of bool Y, f being Function of X, Y st x in meet (("f).:S) holds f.x in meet S; reserve r, s, t, t' for real number; theorem :: PSCOMP_1:3 abs r + abs s = 0 implies r = 0; theorem :: PSCOMP_1:4 r < s & s < t implies abs s < abs r + abs t; theorem :: PSCOMP_1:5 -s < r & r < s implies abs r < s; reserve seq for Real_Sequence, X, Y for Subset of REAL; theorem :: PSCOMP_1:6 seq is convergent & seq is_not_0 & lim seq = 0 implies seq" is non bounded; theorem :: PSCOMP_1:7 rng seq is bounded iff seq is bounded; definition let X be real-membered set; redefine func upper_bound X; synonym sup X; redefine func lower_bound X; synonym inf X; end; definition let X be Subset of REAL; redefine func sup X -> Element of REAL; redefine func inf X -> Element of REAL; end; theorem :: PSCOMP_1:8 for X being non empty real-membered set for t st for s st s in X holds s >= t holds inf X >= t; theorem :: PSCOMP_1:9 for X being non empty real-membered set st (for s st s in X holds s >= r) & for t st for s st s in X holds s >= t holds r >= t holds r = inf X; theorem :: PSCOMP_1:10 for X being non empty real-membered set, r for t st for s st s in X holds s <= t holds sup X <= t; theorem :: PSCOMP_1:11 for X being non empty real-membered set, r st (for s st s in X holds s <= r) & for t st for s st s in X holds s <= t holds r <= t holds r = sup X; theorem :: PSCOMP_1:12 for X being non empty real-membered set, Y being real-membered set st X c= Y & Y is bounded_below holds inf Y <= inf X; theorem :: PSCOMP_1:13 for X being non empty real-membered set, Y being real-membered set st X c= Y & Y is bounded_above holds sup X <= sup Y; definition let X be real-membered set; attr X is with_max means :: PSCOMP_1:def 3 X is bounded_above & sup X in X; attr X is with_min means :: PSCOMP_1:def 4 X is bounded_below & inf X in X; end; definition cluster non empty closed bounded Subset of REAL; end; definition let R be Subset-Family of REAL; attr R is open means :: PSCOMP_1:def 5 for X being Subset of REAL st X in R holds X is open; attr R is closed means :: PSCOMP_1:def 6 for X being Subset of REAL st X in R holds X is closed; end; reserve p, q, r3, r1, r2, q3, p3 for Real; definition let X be Subset of REAL; func -X -> Subset of REAL equals :: PSCOMP_1:def 7 { -r3 : r3 in X}; involutiveness; end; theorem :: PSCOMP_1:14 r in X iff -r in -X; definition let X be non empty Subset of REAL; cluster -X -> non empty; end; theorem :: PSCOMP_1:15 X is bounded_above iff -X is bounded_below; theorem :: PSCOMP_1:16 X is bounded_below iff -X is bounded_above; theorem :: PSCOMP_1:17 for X being non empty Subset of REAL st X is bounded_below holds inf X = - sup -X; theorem :: PSCOMP_1:18 for X being non empty Subset of REAL st X is bounded_above holds sup X = - inf -X; theorem :: PSCOMP_1:19 X is closed iff -X is closed; definition let X be Subset of REAL, p be Real; func p+X -> Subset of REAL equals :: PSCOMP_1:def 8 { p+r3 : r3 in X}; end; theorem :: PSCOMP_1:20 r in X iff q3+r in q3+X; definition let X be non empty Subset of REAL, s be Real; cluster s+X -> non empty; end; theorem :: PSCOMP_1:21 X = 0+X; theorem :: PSCOMP_1:22 q3+(p3+X) = (q3+p3)+X; theorem :: PSCOMP_1:23 X is bounded_above iff q3+X is bounded_above; theorem :: PSCOMP_1:24 X is bounded_below iff q3+X is bounded_below; theorem :: PSCOMP_1:25 for X being non empty Subset of REAL st X is bounded_below holds inf (q3+X) = q3+inf X; theorem :: PSCOMP_1:26 for X being non empty Subset of REAL st X is bounded_above holds sup (q3+X) = q3+sup X; theorem :: PSCOMP_1:27 X is closed iff q3+X is closed; definition let X be Subset of REAL; func Inv X -> Subset of REAL equals :: PSCOMP_1:def 9 { 1/r3 : r3 in X}; end; theorem :: PSCOMP_1:28 for X being without_zero Subset of REAL holds r in X iff 1/r in Inv X; definition let X be non empty without_zero Subset of REAL; cluster Inv X -> non empty without_zero; end; definition let X be without_zero Subset of REAL; cluster Inv X -> without_zero; end; theorem :: PSCOMP_1:29 for X being without_zero Subset of REAL holds Inv Inv X = X; theorem :: PSCOMP_1:30 for X being without_zero Subset of REAL st X is closed & X is bounded holds Inv X is closed; theorem :: PSCOMP_1:31 for Z being Subset-Family of REAL st Z is closed holds meet Z is closed; definition let X be Subset of REAL; func Cl X -> Subset of REAL equals :: PSCOMP_1:def 10 meet { A where A is Element of bool REAL : X c= A & A is closed }; projectivity; end; definition let X be Subset of REAL; cluster Cl X -> closed; end; theorem :: PSCOMP_1:32 for Y being closed Subset of REAL st X c= Y holds Cl X c= Y; theorem :: PSCOMP_1:33 X c= Cl X; theorem :: PSCOMP_1:34 X is closed iff X = Cl X; theorem :: PSCOMP_1:35 Cl ({}REAL) = {}; theorem :: PSCOMP_1:36 Cl ([#]REAL) = REAL; theorem :: PSCOMP_1:37 X c= Y implies Cl X c= Cl Y; theorem :: PSCOMP_1:38 r3 in Cl X iff for O being open Subset of REAL st r3 in O holds O /\ X is non empty; theorem :: PSCOMP_1:39 r3 in Cl X implies ex seq st rng seq c= X & seq is convergent & lim seq = r3; begin :: Functions into Reals definition let X be set, f be Function of X, REAL; redefine attr f is bounded_below means :: PSCOMP_1:def 11 f.:X is bounded_below; attr f is bounded_above means :: PSCOMP_1:def 12 f.:X is bounded_above; end; definition let X be set, f be Function of X, REAL; canceled; attr f is with_max means :: PSCOMP_1:def 14 f.:X is with_max; attr f is with_min means :: PSCOMP_1:def 15 f.:X is with_min; end; definition let X be set, f be Function of X, REAL; func -f -> Function of X, REAL means :: PSCOMP_1:def 16 for p being set st p in X holds it.p = -(f.p); involutiveness; end; theorem :: PSCOMP_1:40 for X, A being set, f being Function of X, REAL holds (-f).:A = -(f.:A); theorem :: PSCOMP_1:41 for X being non empty set, f being Function of X, REAL holds f is with_min iff -f is with_max; theorem :: PSCOMP_1:42 for X being non empty set, f being Function of X, REAL holds f is with_max iff -f is with_min; theorem :: PSCOMP_1:43 for X being set, A being Subset of REAL, f being Function of X, REAL holds (-f)"A = f"(-A); definition let X be set, r be Real, f be Function of X, REAL; func r+f -> Function of X, REAL means :: PSCOMP_1:def 17 for p being set st p in X holds it.p = r+f.p; end; theorem :: PSCOMP_1:44 for X, A being set, f being Function of X, REAL, s being Real holds (s+f).:A = s+(f.:A); theorem :: PSCOMP_1:45 for X being set, A being Subset of REAL, f being Function of X, REAL, q3 holds (q3+f)"A = f"(-q3+A); definition let X be set, f be Function of X, REAL; func Inv f -> Function of X, REAL means :: PSCOMP_1:def 18 for p being set st p in X holds it.p = 1/(f.p); involutiveness; end; theorem :: PSCOMP_1:46 for X being set, A being without_zero Subset of REAL, f being Function of X, REAL holds (Inv f)"A = f"(Inv A); begin :: Real maps definition let T be 1-sorted; mode RealMap of T is Function of the carrier of T, REAL; canceled; end; definition let T be non empty 1-sorted; cluster bounded RealMap of T; end; scheme NonUniqExRF{X() -> non empty TopStruct, P[set,set]}: ex f being RealMap of X() st for x being Element of X() holds P[x, f.x] provided for x being set st x in the carrier of X() ex r3 st P[x, r3]; scheme LambdaRF{X() -> non empty TopStruct, F(set) -> Real}: ex f being RealMap of X() st for x being Element of X() holds f.x = F(x); definition let T be 1-sorted, f be RealMap of T, P be set; redefine func f"P -> Subset of T; end; definition let T be 1-sorted, f be RealMap of T; func inf f -> Real equals :: PSCOMP_1:def 20 inf (f.:the carrier of T); func sup f -> Real equals :: PSCOMP_1:def 21 sup (f.:the carrier of T); end; theorem :: PSCOMP_1:47 for T being non empty TopSpace, f being bounded_below RealMap of T for p being Point of T holds f.p >= inf f; theorem :: PSCOMP_1:48 for T being non empty TopSpace, f being bounded_below RealMap of T for s being Real st for t being Point of T holds f.t >= s holds inf f >= s; theorem :: PSCOMP_1:49 for T being non empty TopSpace, f being RealMap of T st (for p being Point of T holds f.p >= r) & for t st for p being Point of T holds f.p >= t holds r >= t holds r = inf f; theorem :: PSCOMP_1:50 for T being non empty TopSpace, f being bounded_above RealMap of T for p being Point of T holds f.p <= sup f; theorem :: PSCOMP_1:51 for T being non empty TopSpace, f being bounded_above RealMap of T for t st for p being Point of T holds f.p <= t holds sup f <= t; theorem :: PSCOMP_1:52 for T being non empty TopSpace, f being RealMap of T st (for p being Point of T holds f.p <= r) & (for t st for p being Point of T holds f.p <= t holds r <= t) holds r = sup f; theorem :: PSCOMP_1:53 for T being non empty 1-sorted, f being bounded RealMap of T holds inf f <= sup f; definition canceled 3; end; definition let T be TopStruct, f be RealMap of T; attr f is continuous means :: PSCOMP_1:def 25 for Y being Subset of REAL st Y is closed holds f"Y is closed; end; definition let T be non empty TopSpace; cluster continuous RealMap of T; end; definition let T be non empty TopSpace, S be non empty SubSpace of T; cluster continuous RealMap of S; end; reserve T for TopStruct, f for RealMap of T; theorem :: PSCOMP_1:54 f is continuous iff for Y being Subset of REAL st Y is open holds f"Y is open; theorem :: PSCOMP_1:55 f is continuous implies -f is continuous; theorem :: PSCOMP_1:56 f is continuous implies r3+f is continuous; theorem :: PSCOMP_1:57 f is continuous & not 0 in rng f implies Inv f is continuous; definition let X, Y be set, f be Function of bool X, bool Y; let R be Subset-Family of X; redefine func f.:R -> Subset-Family of Y; end; theorem :: PSCOMP_1:58 for R being Subset-Family of REAL st f is continuous & R is open holds ("f).:R is open; theorem :: PSCOMP_1:59 for R being Subset-Family of REAL st f is continuous & R is closed holds ("f).:R is closed; definition let T be non empty TopStruct, X be Subset of T, f be RealMap of T; func f||X -> RealMap of T|X equals :: PSCOMP_1:def 26 f|X; end; definition let T be non empty TopSpace; cluster compact non empty Subset of T; end; definition let T be non empty TopSpace, f be continuous RealMap of T, X be Subset of T; cluster f||X -> continuous; end; definition let T be non empty TopSpace, P be compact non empty Subset of T; cluster T|P -> compact; end; begin :: Pseudocompact spaces theorem :: PSCOMP_1:60 for T being non empty TopSpace holds (for f being RealMap of T st f is continuous holds f is with_max) iff (for f being RealMap of T st f is continuous holds f is with_min); theorem :: PSCOMP_1:61 for T being non empty TopSpace holds (for f being RealMap of T st f is continuous holds f is bounded) iff (for f being RealMap of T st f is continuous holds f is with_max); definition let T be TopStruct; attr T is pseudocompact means :: PSCOMP_1:def 27 for f being RealMap of T st f is continuous holds f is bounded; end; definition cluster compact -> pseudocompact (non empty TopSpace); end; definition cluster compact non empty TopSpace; end; definition let T be pseudocompact non empty TopSpace; cluster continuous -> bounded with_max with_min RealMap of T; end; theorem :: PSCOMP_1:62 for T being non empty TopSpace, X being non empty Subset of T, Y being compact Subset of T, f being continuous RealMap of T st X c= Y holds inf (f||Y) <= inf (f||X); theorem :: PSCOMP_1:63 for T being non empty TopSpace, X being non empty Subset of T, Y being compact Subset of T, f being continuous RealMap of T st X c= Y holds sup (f||X) <= sup (f||Y); begin :: Bounding boxes of compact sets in TOP-REAL 2 definition let n be Nat; let p1, p2 be Point of TOP-REAL n; cluster LSeg(p1,p2) -> compact; end; theorem :: PSCOMP_1:64 for n being Nat, X, Y being compact Subset of TOP-REAL n holds X /\ Y is compact; reserve p for Point of TOP-REAL 2, P for Subset of TOP-REAL 2, Z for non empty Subset of TOP-REAL 2, X for non empty compact Subset of TOP-REAL 2; definition func proj1 -> RealMap of TOP-REAL 2 means :: PSCOMP_1:def 28 for p being Point of TOP-REAL 2 holds it.p = p`1; func proj2 -> RealMap of TOP-REAL 2 means :: PSCOMP_1:def 29 for p being Point of TOP-REAL 2 holds it.p = p`2; end; theorem :: PSCOMP_1:65 proj1"].r,s.[ = {|[ r1, r2 ]| : r < r1 & r1 < s}; theorem :: PSCOMP_1:66 for r3, q3 st P = {|[ r1, r2 ]| : r3 < r1 & r1 < q3} holds P is open; theorem :: PSCOMP_1:67 proj2"].r,s.[ = {|[ r1, r2 ]| : r < r2 & r2 < s}; theorem :: PSCOMP_1:68 for r3, q3 st P = {|[ r1, r2 ]| : r3 < r2 & r2 < q3} holds P is open; definition cluster proj1 -> continuous; cluster proj2 -> continuous; end; theorem :: PSCOMP_1:69 for X being Subset of TOP-REAL 2, p being Point of TOP-REAL 2 st p in X holds (proj1||X).p = p`1; theorem :: PSCOMP_1:70 for X being Subset of TOP-REAL 2, p being Point of TOP-REAL 2 st p in X holds (proj2||X).p = p`2; definition let X be Subset of TOP-REAL 2; func W-bound X -> Real equals :: PSCOMP_1:def 30 inf (proj1||X); func N-bound X -> Real equals :: PSCOMP_1:def 31 sup (proj2||X); func E-bound X -> Real equals :: PSCOMP_1:def 32 sup (proj1||X); func S-bound X -> Real equals :: PSCOMP_1:def 33 inf (proj2||X); end; theorem :: PSCOMP_1:71 p in X implies W-bound X <= p`1 & p`1 <= E-bound X & S-bound X <= p`2 & p`2 <= N-bound X; definition let X be Subset of TOP-REAL 2; func SW-corner X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 34 |[W-bound X, S-bound X]|; func NW-corner X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 35 |[W-bound X, N-bound X]|; func NE-corner X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 36 |[E-bound X, N-bound X]|; func SE-corner X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 37 |[E-bound X, S-bound X]|; end; :: Corners theorem :: PSCOMP_1:72 (SW-corner P)`1 = W-bound P; theorem :: PSCOMP_1:73 (SW-corner P)`2 = S-bound P; theorem :: PSCOMP_1:74 (NW-corner P)`1 = W-bound P; theorem :: PSCOMP_1:75 (NW-corner P)`2 = N-bound P; theorem :: PSCOMP_1:76 (NE-corner P)`1 = E-bound P; theorem :: PSCOMP_1:77 (NE-corner P)`2 = N-bound P; theorem :: PSCOMP_1:78 (SE-corner P)`1 = E-bound P; theorem :: PSCOMP_1:79 (SE-corner P)`2 = S-bound P; theorem :: PSCOMP_1:80 (SW-corner P)`1 = (NW-corner P)`1; theorem :: PSCOMP_1:81 (SE-corner P)`1 = (NE-corner P)`1; theorem :: PSCOMP_1:82 (NW-corner P)`2 = (NE-corner P)`2; theorem :: PSCOMP_1:83 (SW-corner P)`2 = (SE-corner P)`2; definition let X be Subset of TOP-REAL 2; func W-most X -> Subset of TOP-REAL 2 equals :: PSCOMP_1:def 38 LSeg(SW-corner X, NW-corner X)/\X; func N-most X -> Subset of TOP-REAL 2 equals :: PSCOMP_1:def 39 LSeg(NW-corner X, NE-corner X)/\X; func E-most X -> Subset of TOP-REAL 2 equals :: PSCOMP_1:def 40 LSeg(SE-corner X, NE-corner X)/\X; func S-most X -> Subset of TOP-REAL 2 equals :: PSCOMP_1:def 41 LSeg(SW-corner X, SE-corner X)/\X; end; definition let X be non empty compact Subset of TOP-REAL 2; cluster W-most X -> non empty compact; cluster N-most X -> non empty compact; cluster E-most X -> non empty compact; cluster S-most X -> non empty compact; end; definition let X be Subset of TOP-REAL 2; func W-min X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 42 |[W-bound X, inf (proj2||W-most X)]|; func W-max X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 43 |[W-bound X, sup (proj2||W-most X)]|; func N-min X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 44 |[inf (proj1||N-most X), N-bound X]|; func N-max X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 45 |[sup (proj1||N-most X), N-bound X]|; func E-max X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 46 |[E-bound X, sup (proj2||E-most X)]|; func E-min X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 47 |[E-bound X, inf (proj2||E-most X)]|; func S-max X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 48 |[sup (proj1||S-most X), S-bound X]|; func S-min X -> Point of TOP-REAL 2 equals :: PSCOMP_1:def 49 |[inf (proj1||S-most X), S-bound X]|; end; theorem :: PSCOMP_1:84 (W-min P)`1 = W-bound P & (W-max P)`1 = W-bound P; theorem :: PSCOMP_1:85 (SW-corner P)`1 = (W-min P)`1 & (SW-corner P)`1 = (W-max P)`1 & (W-min P)`1 = (W-max P)`1 & (W-min P)`1 = (NW-corner P)`1 & (W-max P)`1 = (NW-corner P)`1; theorem :: PSCOMP_1:86 (W-min P)`2 = inf (proj2||W-most P) & (W-max P)`2 = sup (proj2||W-most P); theorem :: PSCOMP_1:87 (SW-corner X)`2 <= (W-min X)`2 & (SW-corner X)`2 <= (W-max X)`2 & (SW-corner X)`2 <= (NW-corner X)`2 & (W-min X)`2 <= (W-max X)`2 & (W-min X)`2 <= (NW-corner X)`2 & (W-max X)`2 <= (NW-corner X)`2; theorem :: PSCOMP_1:88 p in W-most Z implies p`1 = (W-min Z)`1 & (Z is compact implies (W-min Z)`2 <= p`2 & p`2 <= (W-max Z)`2); theorem :: PSCOMP_1:89 W-most X c= LSeg(W-min X, W-max X); theorem :: PSCOMP_1:90 LSeg(W-min X, W-max X) c= LSeg(SW-corner X, NW-corner X); theorem :: PSCOMP_1:91 W-min X in W-most X & W-max X in W-most X; theorem :: PSCOMP_1:92 LSeg(SW-corner X, W-min X)/\X = {W-min X} & LSeg(W-max X, NW-corner X)/\X = {W-max X}; theorem :: PSCOMP_1:93 W-min X = W-max X implies W-most X = {W-min X}; :: North theorem :: PSCOMP_1:94 (N-min P)`2 = N-bound P & (N-max P)`2 = N-bound P; theorem :: PSCOMP_1:95 (NW-corner P)`2 = (N-min P)`2 & (NW-corner P)`2 = (N-max P)`2 & (N-min P)`2 = (N-max P)`2 & (N-min P)`2 = (NE-corner P)`2 & (N-max P)`2 = (NE-corner P)`2; theorem :: PSCOMP_1:96 (N-min P)`1 = inf (proj1||N-most P) & (N-max P)`1 = sup (proj1||N-most P); theorem :: PSCOMP_1:97 (NW-corner X)`1 <= (N-min X)`1 & (NW-corner X)`1 <= (N-max X)`1 & (NW-corner X)`1 <= (NE-corner X)`1 & (N-min X)`1 <= (N-max X)`1 & (N-min X)`1 <= (NE-corner X)`1 & (N-max X)`1 <= (NE-corner X)`1; theorem :: PSCOMP_1:98 p in N-most Z implies p`2 = (N-min Z)`2 & (Z is compact implies (N-min Z)`1 <= p`1 & p`1 <= (N-max Z)`1); theorem :: PSCOMP_1:99 N-most X c= LSeg(N-min X, N-max X); theorem :: PSCOMP_1:100 LSeg(N-min X, N-max X) c= LSeg(NW-corner X, NE-corner X); theorem :: PSCOMP_1:101 N-min X in N-most X & N-max X in N-most X; theorem :: PSCOMP_1:102 LSeg(NW-corner X, N-min X)/\X = {N-min X} & LSeg(N-max X, NE-corner X)/\X = {N-max X}; theorem :: PSCOMP_1:103 N-min X = N-max X implies N-most X = {N-min X}; :: East theorem :: PSCOMP_1:104 (E-min P)`1 = E-bound P & (E-max P)`1 = E-bound P; theorem :: PSCOMP_1:105 (SE-corner P)`1 = (E-min P)`1 & (SE-corner P)`1 = (E-max P)`1 & (E-min P)`1 = (E-max P)`1 & (E-min P)`1 = (NE-corner P)`1 & (E-max P)`1 = (NE-corner P)`1; theorem :: PSCOMP_1:106 (E-min P)`2 = inf (proj2||E-most P) & (E-max P)`2 = sup (proj2||E-most P); theorem :: PSCOMP_1:107 (SE-corner X)`2 <= (E-min X)`2 & (SE-corner X)`2 <= (E-max X)`2 & (SE-corner X)`2 <= (NE-corner X)`2 & (E-min X)`2 <= (E-max X)`2 & (E-min X)`2 <= (NE-corner X)`2 & (E-max X)`2 <= (NE-corner X)`2; theorem :: PSCOMP_1:108 p in E-most Z implies p`1 = (E-min Z)`1 & (Z is compact implies (E-min Z)`2 <= p`2 & p`2 <= (E-max Z)`2); theorem :: PSCOMP_1:109 E-most X c= LSeg(E-min X, E-max X); theorem :: PSCOMP_1:110 LSeg(E-min X, E-max X) c= LSeg(SE-corner X, NE-corner X); theorem :: PSCOMP_1:111 E-min X in E-most X & E-max X in E-most X; theorem :: PSCOMP_1:112 LSeg(SE-corner X, E-min X)/\X = {E-min X} & LSeg(E-max X, NE-corner X)/\X = {E-max X}; theorem :: PSCOMP_1:113 E-min X = E-max X implies E-most X = {E-min X}; :: South theorem :: PSCOMP_1:114 (S-min P)`2 = S-bound P & (S-max P)`2 = S-bound P; theorem :: PSCOMP_1:115 (SW-corner P)`2 = (S-min P)`2 & (SW-corner P)`2 = (S-max P)`2 & (S-min P)`2 = (S-max P)`2 & (S-min P)`2 = (SE-corner P)`2 & (S-max P)`2 = (SE-corner P)`2; theorem :: PSCOMP_1:116 (S-min P)`1 = inf (proj1||S-most P) & (S-max P)`1 = sup (proj1||S-most P); theorem :: PSCOMP_1:117 (SW-corner X)`1 <= (S-min X)`1 & (SW-corner X)`1 <= (S-max X)`1 & (SW-corner X)`1 <= (SE-corner X)`1 & (S-min X)`1 <= (S-max X)`1 & (S-min X)`1 <= (SE-corner X)`1 & (S-max X)`1 <= (SE-corner X)`1; theorem :: PSCOMP_1:118 p in S-most Z implies p`2 = (S-min Z)`2 & (Z is compact implies (S-min Z)`1 <= p`1 & p`1 <= (S-max Z)`1); theorem :: PSCOMP_1:119 S-most X c= LSeg(S-min X, S-max X); theorem :: PSCOMP_1:120 LSeg(S-min X, S-max X) c= LSeg(SW-corner X, SE-corner X); theorem :: PSCOMP_1:121 S-min X in S-most X & S-max X in S-most X; theorem :: PSCOMP_1:122 LSeg(SW-corner X, S-min X)/\X = {S-min X} & LSeg(S-max X, SE-corner X)/\X = {S-max X}; theorem :: PSCOMP_1:123 S-min X = S-max X implies S-most X = {S-min X}; :: Degenerate cases theorem :: PSCOMP_1:124 W-max P = N-min P implies W-max P = NW-corner P; theorem :: PSCOMP_1:125 N-max P = E-max P implies N-max P = NE-corner P; theorem :: PSCOMP_1:126 E-min P = S-max P implies E-min P = SE-corner P; theorem :: PSCOMP_1:127 S-min P = W-min P implies S-min P = SW-corner P;

Back to top