The Mizar abstract of SPRECT

Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users
The abstract of the Mizar article:: On the Rectangular Finite Sequences of the Points of the Plane
by
Andrzej Trybulec, and
Yatsuka Nakamura
Received November 30, 1997
MML identifier: SPRECT_1
[ Mizar article, MML identifier index ]
environ

 vocabulary REALSET1, SEQM_3, FUNCT_1, RELAT_1, FUNCOP_1, BOOLE, FINSEQ_1,
      PRE_TOPC, CONNSP_1, EUCLID, COMPTS_1, TOPREAL1, SPPOL_1, MCART_1,
      SPPOL_2, PSCOMP_1, FINSEQ_6, GOBOARD5, GOBOARD1, CARD_1, ORDINAL2,
      GOBOARD2, MATRIX_2, TREES_1, MATRIX_1, ABSVALUE, ARYTM_1, RCOMP_1, SEQ_2,
      FUNCT_5, SQUARE_1, LATTICES, ARYTM_3, JORDAN1, SUBSET_1, GOBOARD9,
      TOPS_1, SPRECT_1, FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, ORDINAL1,
      NUMBERS, XREAL_0, REAL_1, NAT_1, ABSVALUE, CARD_1, FUNCOP_1, SQUARE_1,
      FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_4, FINSEQ_6, SEQM_3, SEQ_4, MATRIX_1,
      MATRIX_2, REALSET1, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1,
      CONNSP_1, EUCLID, TOPREAL1, JORDAN1, GOBOARD1, GOBOARD2, GOBOARD5,
      GOBOARD9, SPPOL_1, SPPOL_2, PSCOMP_1;
 constructors PSCOMP_1, NAT_1, SPPOL_1, SPPOL_2, TOPREAL4, REALSET1, GOBOARD2,
      ENUMSET1, MATRIX_2, REAL_1, ABSVALUE, GOBOARD9, JORDAN1, CONNSP_1,
      TOPS_1, FUNCOP_1, SQUARE_1, RCOMP_1, FINSEQ_4, COMPTS_1, PARTFUN1;
 clusters STRUCT_0, EUCLID, PSCOMP_1, RELSET_1, FINSEQ_6, YELLOW_6, GOBOARD2,
      FINSEQ_5, GOBOARD9, TEX_2, RELAT_1, GOBOARD5, PRE_TOPC, WAYBEL_2,
      TOPREAL1, FINSEQ_1, REALSET1, XBOOLE_0, SEQ_2, NAT_1, MEMBERED, SEQM_3;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

theorem :: SPRECT_1:1
 for A being trivial set
  for B being set st B c= A holds B is trivial;

definition
 cluster non constant -> non trivial Function;
end;

definition
 cluster trivial -> constant Function;
end;

theorem :: SPRECT_1:2
 for f being Function st rng f is trivial holds f is constant;

definition let f be constant Function;
 cluster rng f -> trivial;
end;

definition
 cluster non empty constant FinSequence;
end;

theorem :: SPRECT_1:3
 for f,g being FinSequence st f^g is constant
  holds f is constant & g is constant;

theorem :: SPRECT_1:4
 for x,y being set st <*x,y*> is constant
  holds x = y;

theorem :: SPRECT_1:5
 for x,y,z being set st <*x,y,z*> is constant
  holds x = y & y = z & z = x;

begin :: Topology

theorem :: SPRECT_1:6
 for GX being non empty TopSpace,
     A being Subset of GX,
     B being non empty Subset of GX
 holds A is_a_component_of B implies A <> {};

theorem :: SPRECT_1:7
 for GX being TopStruct,
     A, B being Subset of GX
 holds A is_a_component_of B implies A c= B;

theorem :: SPRECT_1:8
 for T being non empty TopSpace,
     A being non empty Subset of T,
     B1,B2,S being Subset of T
  st B1 is_a_component_of A & B2 is_a_component_of A &
     S is_a_component_of A & B1 \/ B2 = A
 holds S = B1 or S = B2;

theorem :: SPRECT_1:9
 for T being non empty TopSpace,
     A being non empty Subset of T,
     B1,B2,C1,C2 being Subset of T
  st B1 is_a_component_of A & B2 is_a_component_of A &
     C1 is_a_component_of A & C2 is_a_component_of A &
     B1 \/ B2 = A & C1 \/ C2 = A
 holds { B1,B2 } = { C1,C2 };

begin :: Topology of Plane

reserve S for Subset of TOP-REAL 2,
        C,C1,C2 for non empty compact Subset of TOP-REAL 2,
        p,q for Point of TOP-REAL 2;

theorem :: SPRECT_1:10
 for p,q,r being Point of TOP-REAL 2
  holds L~<*p,q,r*> = LSeg(p,q) \/ LSeg(q,r);

definition let n be Nat; let f be non trivial FinSequence of TOP-REAL n;
 cluster L~f -> non empty;
end;

definition let f be FinSequence of TOP-REAL 2;
 cluster L~f -> compact;
end;

theorem :: SPRECT_1:11
 for A,B being Subset of TOP-REAL 2 st A c= B & B is horizontal
 holds A is horizontal;

theorem :: SPRECT_1:12
 for A,B being Subset of TOP-REAL 2 st A c= B & B is vertical
 holds A is vertical;

definition
 cluster R^2-unit_square -> special_polygonal non horizontal non vertical;
end;

definition
 cluster non vertical non horizontal non empty compact Subset of TOP-REAL 2;
end;

begin :: Special points of a compact non empty subset of the plane

theorem :: SPRECT_1:13
 N-min C in C & N-max C in C;

theorem :: SPRECT_1:14
 S-min C in C & S-max C in C;

theorem :: SPRECT_1:15
 W-min C in C & W-max C in C;

theorem :: SPRECT_1:16
 E-min C in C & E-max C in C;

theorem :: SPRECT_1:17
 C is vertical iff W-bound C = E-bound C;

theorem :: SPRECT_1:18
 C is horizontal iff S-bound C = N-bound C;

theorem :: SPRECT_1:19
   NW-corner C = NE-corner C implies C is vertical;

theorem :: SPRECT_1:20
   SW-corner C = SE-corner C implies C is vertical;

theorem :: SPRECT_1:21
   NW-corner C = SW-corner C implies C is horizontal;

theorem :: SPRECT_1:22
   NE-corner C = SE-corner C implies C is horizontal;

 reserve i,j,k for Nat,
         t,r1,r2,s1,s2 for Real;

theorem :: SPRECT_1:23
 W-bound C <= E-bound C;

theorem :: SPRECT_1:24
 S-bound C <= N-bound C;

theorem :: SPRECT_1:25
 LSeg(SE-corner C, NE-corner C) =
  { p : p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C };

theorem :: SPRECT_1:26
  LSeg(SW-corner C, SE-corner C) =
    { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C};

theorem :: SPRECT_1:27
 LSeg(NW-corner C, NE-corner C) =
  { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C};

theorem :: SPRECT_1:28
   LSeg(SW-corner C, NW-corner C) =
     { p : p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C};

theorem :: SPRECT_1:29
   LSeg(SW-corner C,NW-corner C) /\ LSeg(NW-corner C,NE-corner C) = {NW-corner
C
};

theorem :: SPRECT_1:30
 LSeg(NW-corner C,NE-corner C) /\ LSeg(NE-corner C,SE-corner C) = {NE-corner C}
;

theorem :: SPRECT_1:31
 LSeg(SE-corner C,NE-corner C) /\ LSeg(SW-corner C,SE-corner C) = {SE-corner C}
;

theorem :: SPRECT_1:32
 LSeg(NW-corner C,SW-corner C) /\ LSeg(SW-corner C,SE-corner C) = {SW-corner C}
;

begin :: Neither vertical nor horizontal

reserve D1 for non vertical non empty compact Subset of TOP-REAL 2,
        D2 for non horizontal non empty compact Subset of TOP-REAL 2,
        D for non vertical non horizontal non empty compact
              Subset of TOP-REAL 2;

theorem :: SPRECT_1:33
 W-bound D1 < E-bound D1;

theorem :: SPRECT_1:34
 S-bound D2 < N-bound D2;

theorem :: SPRECT_1:35
 LSeg(SW-corner D1,NW-corner D1) misses LSeg(SE-corner D1,NE-corner D1);

theorem :: SPRECT_1:36
 LSeg(SW-corner D2,SE-corner D2) misses LSeg(NW-corner D2,NE-corner D2);

begin :: SpStSeq

definition let C be Subset of TOP-REAL 2;
 func SpStSeq C -> FinSequence of TOP-REAL 2 equals
:: SPRECT_1:def 1
 <*NW-corner C,NE-corner C,SE-corner C*>^
      <*SW-corner C,NW-corner C*>;
end;

theorem :: SPRECT_1:37
 (SpStSeq S)/.1 = NW-corner S;

theorem :: SPRECT_1:38
 (SpStSeq S)/.2 = NE-corner S;

theorem :: SPRECT_1:39
 (SpStSeq S)/.3 = SE-corner S;

theorem :: SPRECT_1:40
 (SpStSeq S)/.4 = SW-corner S;

theorem :: SPRECT_1:41
   (SpStSeq S)/.5 = NW-corner S;

theorem :: SPRECT_1:42
 len SpStSeq S = 5;

theorem :: SPRECT_1:43
 L~SpStSeq S =
   (LSeg(NW-corner S,NE-corner S) \/ LSeg(NE-corner S,SE-corner S)) \/
   (LSeg(SE-corner S,SW-corner S) \/ LSeg(SW-corner S,NW-corner S));

definition let D be non vertical non empty compact Subset of TOP-REAL 2;
 cluster SpStSeq D -> non constant;
end;

definition let D be non horizontal non empty compact Subset of TOP-REAL 2;
 cluster SpStSeq D -> non constant;
end;

definition let D be non vertical non horizontal non empty compact
                    Subset of TOP-REAL 2;
 cluster SpStSeq D -> special unfolded circular s.c.c. standard;
end;

theorem :: SPRECT_1:44
 L~SpStSeq D = [.W-bound D,E-bound D,S-bound D,N-bound D.];

:::: Special points of SpStSeq D (or C)

theorem :: SPRECT_1:45
 for T being non empty TopStruct, X being Subset of T,
     f be RealMap of T
 holds rng(f||X) = f.:X;

theorem :: SPRECT_1:46
 for T being non empty TopSpace, X being non empty compact Subset of T,
     f be continuous RealMap of T
 holds f.:X is bounded_below;

theorem :: SPRECT_1:47
 for T being non empty TopSpace, X being non empty compact Subset of T,
     f be continuous RealMap of T
 holds f.:X is bounded_above;

definition
 cluster non empty bounded_above bounded_below Subset of REAL;
end;

theorem :: SPRECT_1:48
 W-bound S = inf(proj1.:S);

theorem :: SPRECT_1:49
 S-bound S = inf(proj2.:S);

theorem :: SPRECT_1:50
 N-bound S = sup(proj2.:S);

theorem :: SPRECT_1:51
 E-bound S = sup(proj1.:S);

theorem :: SPRECT_1:52
 for A,B being non empty bounded_below Subset of REAL
  holds inf(A \/ B) = min(inf A,inf B);

theorem :: SPRECT_1:53
 for A,B being non empty bounded_above Subset of REAL
  holds sup(A \/ B) = max(sup A,sup B);

theorem :: SPRECT_1:54
 S = C1 \/ C2 implies W-bound S = min(W-bound C1, W-bound C2);

theorem :: SPRECT_1:55
 S = C1 \/ C2 implies S-bound S = min(S-bound C1, S-bound C2);

theorem :: SPRECT_1:56
 S = C1 \/ C2 implies N-bound S = max(N-bound C1, N-bound C2);

theorem :: SPRECT_1:57
 S = C1 \/ C2 implies E-bound S = max(E-bound C1, E-bound C2);

definition let p,q;
 cluster LSeg(p,q) -> compact;
end;

definition
 cluster {}REAL -> bounded;
end;

definition let r1,r2;
 cluster [.r1,r2.] -> bounded;
end;

definition
 cluster bounded -> bounded_below bounded_above Subset of REAL;
 cluster bounded_below bounded_above -> bounded Subset of REAL;
end;

canceled;

theorem :: SPRECT_1:59
 r1 <= r2 implies
  (t in [.r1,r2.] iff ex s1 st 0 <=s1 & s1 <= 1 & t = s1*r1 + (1-s1)*r2);

theorem :: SPRECT_1:60
 p`1 <= q`1 implies proj1.:LSeg(p,q) = [.p`1,q`1.];

theorem :: SPRECT_1:61
 p`2 <= q`2 implies proj2.:LSeg(p,q) = [.p`2,q`2.];

theorem :: SPRECT_1:62
 p`1 <= q`1 implies W-bound LSeg(p,q) = p`1;

theorem :: SPRECT_1:63
 p`2 <= q`2 implies S-bound LSeg(p,q) = p`2;

theorem :: SPRECT_1:64
 p`2 <= q`2 implies N-bound LSeg(p,q) = q`2;

theorem :: SPRECT_1:65
 p`1 <= q`1 implies E-bound LSeg(p,q) = q`1;

theorem :: SPRECT_1:66
 W-bound L~SpStSeq C = W-bound C;

theorem :: SPRECT_1:67
 S-bound L~SpStSeq C = S-bound C;

theorem :: SPRECT_1:68
 N-bound L~SpStSeq C = N-bound C;

theorem :: SPRECT_1:69
 E-bound L~SpStSeq C = E-bound C;

theorem :: SPRECT_1:70
  NW-corner L~SpStSeq C = NW-corner C;

theorem :: SPRECT_1:71
  NE-corner L~SpStSeq C = NE-corner C;

theorem :: SPRECT_1:72
  SW-corner L~SpStSeq C = SW-corner C;

theorem :: SPRECT_1:73
  SE-corner L~SpStSeq C = SE-corner C;

theorem :: SPRECT_1:74
 W-most L~SpStSeq C = LSeg(SW-corner C,NW-corner C);

theorem :: SPRECT_1:75
 N-most L~SpStSeq C = LSeg(NW-corner C,NE-corner C);

theorem :: SPRECT_1:76
 S-most L~SpStSeq C = LSeg(SW-corner C,SE-corner C);

theorem :: SPRECT_1:77
 E-most L~SpStSeq C = LSeg(SE-corner C,NE-corner C);

theorem :: SPRECT_1:78
 proj2.:LSeg(SW-corner C,NW-corner C) = [.S-bound C,N-bound C.];

theorem :: SPRECT_1:79
 proj1.:LSeg(NW-corner C,NE-corner C) = [.W-bound C,E-bound C.];

theorem :: SPRECT_1:80
 proj2.:LSeg(NE-corner C,SE-corner C) = [.S-bound C,N-bound C.];

theorem :: SPRECT_1:81
 proj1.:LSeg(SE-corner C,SW-corner C) = [.W-bound C,E-bound C.];

theorem :: SPRECT_1:82
 W-min L~SpStSeq C = SW-corner C;

theorem :: SPRECT_1:83
 W-max L~SpStSeq C = NW-corner C;

theorem :: SPRECT_1:84
 N-min L~SpStSeq C = NW-corner C;

theorem :: SPRECT_1:85
 N-max L~SpStSeq C = NE-corner C;

theorem :: SPRECT_1:86
 E-min L~SpStSeq C = SE-corner C;

theorem :: SPRECT_1:87
 E-max L~SpStSeq C = NE-corner C;

theorem :: SPRECT_1:88
 S-min L~SpStSeq C = SW-corner C;

theorem :: SPRECT_1:89
 S-max L~SpStSeq C = SE-corner C;

begin :: rectangular

definition let f be FinSequence of TOP-REAL 2;
 attr f is rectangular means
:: SPRECT_1:def 2
 ex D st f = SpStSeq D;
end;

definition let D;
 cluster SpStSeq D -> rectangular;
end;

definition
 cluster rectangular FinSequence of TOP-REAL 2;
end;

reserve s for rectangular FinSequence of TOP-REAL 2;

theorem :: SPRECT_1:90
   len s = 5;

definition
 cluster rectangular -> non constant FinSequence of TOP-REAL 2;
end;

definition
 cluster rectangular ->
     standard special unfolded circular s.c.c.
       (non empty FinSequence of TOP-REAL 2);
end;

:::: Special points of L~f, f - rectangular

theorem :: SPRECT_1:91
   s/.1 = N-min L~s & s/.1 = W-max L~s;

theorem :: SPRECT_1:92
   s/.2 = N-max L~s & s/.2 = E-max L~s;

theorem :: SPRECT_1:93
   s/.3 = S-max L~s & s/.3 = E-min L~s;

theorem :: SPRECT_1:94
   s/.4 = S-min L~s & s/.4 = W-min L~s;

begin :: Jordan

theorem :: SPRECT_1:95
  r1 < r2 & s1 < s2 implies [.r1,r2,s1,s2.] is Jordan;

definition let f be rectangular FinSequence of TOP-REAL 2;
 cluster L~f -> Jordan;
end;

definition let S be Subset of TOP-REAL 2;
 redefine attr S is Jordan means
:: SPRECT_1:def 3
 S`<> {} &
 ex A1,A2 being Subset of TOP-REAL 2
  st S` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 &
     A1 is_a_component_of S` & A2 is_a_component_of S`;
end;

theorem :: SPRECT_1:96
 for f being rectangular FinSequence of TOP-REAL 2
  holds LeftComp f misses RightComp f;

definition let f be non constant standard special_circular_sequence;
 cluster LeftComp f -> non empty;
 cluster RightComp f -> non empty;
end;

theorem :: SPRECT_1:97
   for f being rectangular FinSequence of TOP-REAL 2
  holds LeftComp f <> RightComp f;
The abstract of the Mizar article:

On the Rectangular Finite Sequences of the Points of the Plane
