:: On Rectangular Finite Sequences of the Points of the Plane
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Copyright (c) 1997-2021 Association of Mizar Users

registration
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is constant )
proof end;
end;

theorem Th1: :: SPRECT_1:1
for f, g being FinSequence st f ^ g is constant holds
( f is constant & g is constant )
proof end;

theorem Th2: :: SPRECT_1:2
for x, y being set st <*x,y*> is constant holds
x = y
proof end;

theorem Th3: :: SPRECT_1:3
for x, y, z being set st <*x,y,z*> is constant holds
( x = y & y = z & z = x )
proof end;

theorem Th4: :: SPRECT_1:4
for GX being non empty TopSpace
for A being Subset of GX
for B being non empty Subset of GX st A is_a_component_of B holds
A <> {}
proof end;

theorem Th5: :: SPRECT_1:5
for GX being TopStruct
for A, B being Subset of GX st A is_a_component_of B holds
A c= B
proof end;

theorem Th6: :: SPRECT_1:6
for T being non empty TopSpace
for A being non empty Subset of T
for 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 & not S = B1 holds
S = B2
proof end;

theorem Th7: :: SPRECT_1:7
for T being non empty TopSpace
for A being non empty Subset of T
for 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}
proof end;

theorem Th8: :: SPRECT_1:8
for p, q, r being Point of () holds L~ <*p,q,r*> = (LSeg (p,q)) \/ (LSeg (q,r))
proof end;

registration
let n be Nat;
let f be non trivial FinSequence of ();
cluster L~ f -> non empty ;
coherence
not L~ f is empty
proof end;
end;

registration
let f be FinSequence of ();
cluster L~ f -> compact ;
coherence
L~ f is compact
proof end;
end;

theorem Th9: :: SPRECT_1:9
for A, B being Subset of () st A c= B & B is horizontal holds
A is horizontal ;

theorem Th10: :: SPRECT_1:10
for A, B being Subset of () st A c= B & B is vertical holds
A is vertical ;

registration
coherence
( R^2-unit_square is special_polygonal & not R^2-unit_square is horizontal & not R^2-unit_square is vertical )
proof end;
end;

registration
cluster non empty compact non horizontal non vertical for Element of bool the carrier of ();
existence
ex b1 being Subset of () st
( not b1 is vertical & not b1 is horizontal & not b1 is empty & b1 is compact )
proof end;
end;

theorem Th11: :: SPRECT_1:11
for C being non empty compact Subset of () holds
( N-min C in C & N-max C in C )
proof end;

theorem Th12: :: SPRECT_1:12
for C being non empty compact Subset of () holds
( S-min C in C & S-max C in C )
proof end;

theorem Th13: :: SPRECT_1:13
for C being non empty compact Subset of () holds
( W-min C in C & W-max C in C )
proof end;

theorem Th14: :: SPRECT_1:14
for C being non empty compact Subset of () holds
( E-min C in C & E-max C in C )
proof end;

theorem Th15: :: SPRECT_1:15
for C being non empty compact Subset of () holds
( C is vertical iff W-bound C = E-bound C )
proof end;

theorem Th16: :: SPRECT_1:16
for C being non empty compact Subset of () holds
( C is horizontal iff S-bound C = N-bound C )
proof end;

theorem :: SPRECT_1:17
for C being non empty compact Subset of () st NW-corner C = NE-corner C holds
C is vertical
proof end;

theorem :: SPRECT_1:18
for C being non empty compact Subset of () st SW-corner C = SE-corner C holds
C is vertical
proof end;

theorem :: SPRECT_1:19
for C being non empty compact Subset of () st NW-corner C = SW-corner C holds
C is horizontal
proof end;

theorem :: SPRECT_1:20
for C being non empty compact Subset of () st NE-corner C = SE-corner C holds
C is horizontal
proof end;

theorem Th21: :: SPRECT_1:21
for C being non empty compact Subset of () holds W-bound C <= E-bound C
proof end;

theorem Th22: :: SPRECT_1:22
for C being non empty compact Subset of () holds S-bound C <= N-bound C
proof end;

theorem Th23: :: SPRECT_1:23
for C being non empty compact Subset of () holds LSeg ((),()) = { p where p is Point of () : ( p 1 = E-bound C & p 2 <= N-bound C & p 2 >= S-bound C ) }
proof end;

theorem Th24: :: SPRECT_1:24
for C being non empty compact Subset of () holds LSeg ((),()) = { p where p is Point of () : ( p 1 <= E-bound C & p 1 >= W-bound C & p 2 = S-bound C ) }
proof end;

theorem Th25: :: SPRECT_1:25
for C being non empty compact Subset of () holds LSeg ((),()) = { p where p is Point of () : ( p 1 <= E-bound C & p 1 >= W-bound C & p 2 = N-bound C ) }
proof end;

theorem Th26: :: SPRECT_1:26
for C being non empty compact Subset of () holds LSeg ((),()) = { p where p is Point of () : ( p 1 = W-bound C & p 2 <= N-bound C & p 2 >= S-bound C ) }
proof end;

theorem :: SPRECT_1:27
for C being non empty compact Subset of () holds (LSeg ((),())) /\ (LSeg ((),())) = {()}
proof end;

theorem Th28: :: SPRECT_1:28
for C being non empty compact Subset of () holds (LSeg ((),())) /\ (LSeg ((),())) = {()}
proof end;

theorem Th29: :: SPRECT_1:29
for C being non empty compact Subset of () holds (LSeg ((),())) /\ (LSeg ((),())) = {()}
proof end;

theorem Th30: :: SPRECT_1:30
for C being non empty compact Subset of () holds (LSeg ((),())) /\ (LSeg ((),())) = {()}
proof end;

theorem Th31: :: SPRECT_1:31
for D1 being non empty compact non vertical Subset of () holds W-bound D1 < E-bound D1
proof end;

theorem Th32: :: SPRECT_1:32
for D2 being non empty compact non horizontal Subset of () holds S-bound D2 < N-bound D2
proof end;

theorem Th33: :: SPRECT_1:33
for D1 being non empty compact non vertical Subset of () holds LSeg ((),()) misses LSeg ((),())
proof end;

theorem Th34: :: SPRECT_1:34
for D2 being non empty compact non horizontal Subset of () holds LSeg ((),()) misses LSeg ((),())
proof end;

definition
let C be Subset of ();
func SpStSeq C -> FinSequence of () equals :: SPRECT_1:def 1
<*(),(),()*> ^ <*(),()*>;
coherence
<*(),(),()*> ^ <*(),()*> is FinSequence of ()
;
end;

:: deftheorem defines SpStSeq SPRECT_1:def 1 :
for C being Subset of () holds SpStSeq C = <*(),(),()*> ^ <*(),()*>;

theorem Th35: :: SPRECT_1:35
for S being Subset of () holds () /. 1 = NW-corner S
proof end;

theorem Th36: :: SPRECT_1:36
for S being Subset of () holds () /. 2 = NE-corner S
proof end;

theorem Th37: :: SPRECT_1:37
for S being Subset of () holds () /. 3 = SE-corner S
proof end;

theorem Th38: :: SPRECT_1:38
for S being Subset of () holds () /. 4 = SW-corner S
proof end;

theorem :: SPRECT_1:39
for S being Subset of () holds () /. 5 = NW-corner S
proof end;

theorem Th40: :: SPRECT_1:40
for S being Subset of () holds len () = 5
proof end;

theorem Th41: :: SPRECT_1:41
for S being Subset of () holds L~ () = ((LSeg ((),())) \/ (LSeg ((),()))) \/ ((LSeg ((),())) \/ (LSeg ((),())))
proof end;

registration
let D be non empty compact non vertical Subset of ();
cluster SpStSeq D -> non constant ;
coherence
not SpStSeq D is constant
proof end;
end;

registration
let D be non empty compact non horizontal Subset of ();
cluster SpStSeq D -> non constant ;
coherence
not SpStSeq D is constant
proof end;
end;

registration
let D be non empty compact non horizontal non vertical Subset of ();
coherence
( SpStSeq D is special & SpStSeq D is unfolded & SpStSeq D is circular & SpStSeq D is s.c.c. & SpStSeq D is standard )
proof end;
end;

theorem Th42: :: SPRECT_1:42
for D being non empty compact non horizontal non vertical Subset of () holds L~ () = [.(),(),(),().]
proof end;

registration
let T be non empty TopSpace;
let X be non empty compact Subset of T;
let f be continuous RealMap of T;
coherence
f .: X is bounded_below
proof end;
coherence
f .: X is bounded_above
proof end;
end;

theorem Th43: :: SPRECT_1:43
for S being Subset of () holds W-bound S = lower_bound ()
proof end;

theorem Th44: :: SPRECT_1:44
for S being Subset of () holds S-bound S = lower_bound ()
proof end;

theorem Th45: :: SPRECT_1:45
for S being Subset of () holds N-bound S = upper_bound ()
proof end;

theorem Th46: :: SPRECT_1:46
for S being Subset of () holds E-bound S = upper_bound ()
proof end;

theorem Th47: :: SPRECT_1:47
for S being Subset of ()
for C1, C2 being non empty compact Subset of () st S = C1 \/ C2 holds
W-bound S = min ((W-bound C1),(W-bound C2))
proof end;

theorem Th48: :: SPRECT_1:48
for S being Subset of ()
for C1, C2 being non empty compact Subset of () st S = C1 \/ C2 holds
S-bound S = min ((S-bound C1),(S-bound C2))
proof end;

theorem Th49: :: SPRECT_1:49
for S being Subset of ()
for C1, C2 being non empty compact Subset of () st S = C1 \/ C2 holds
N-bound S = max ((N-bound C1),(N-bound C2))
proof end;

theorem Th50: :: SPRECT_1:50
for S being Subset of ()
for C1, C2 being non empty compact Subset of () st S = C1 \/ C2 holds
E-bound S = max ((E-bound C1),(E-bound C2))
proof end;

registration
let r1, r2 be Real;
cluster K74(r1,r2) -> real-bounded for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = [.r1,r2.] holds
b1 is real-bounded
proof end;
end;

theorem Th51: :: SPRECT_1:51
for t, r1, r2 being Real st r1 <= r2 holds
( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )
proof end;

theorem Th52: :: SPRECT_1:52
for p, q being Point of () st p 1 <= q 1 holds
proj1 .: (LSeg (p,q)) = [.(p 1),(q 1).]
proof end;

theorem Th53: :: SPRECT_1:53
for p, q being Point of () st p 2 <= q 2 holds
proj2 .: (LSeg (p,q)) = [.(p 2),(q 2).]
proof end;

theorem Th54: :: SPRECT_1:54
for p, q being Point of () st p 1 <= q 1 holds
W-bound (LSeg (p,q)) = p 1
proof end;

theorem Th55: :: SPRECT_1:55
for p, q being Point of () st p 2 <= q 2 holds
S-bound (LSeg (p,q)) = p 2
proof end;

theorem Th56: :: SPRECT_1:56
for p, q being Point of () st p 2 <= q 2 holds
N-bound (LSeg (p,q)) = q 2
proof end;

theorem Th57: :: SPRECT_1:57
for p, q being Point of () st p 1 <= q 1 holds
E-bound (LSeg (p,q)) = q 1
proof end;

theorem Th58: :: SPRECT_1:58
for C being non empty compact Subset of () holds W-bound (L~ ()) = W-bound C
proof end;

theorem Th59: :: SPRECT_1:59
for C being non empty compact Subset of () holds S-bound (L~ ()) = S-bound C
proof end;

theorem Th60: :: SPRECT_1:60
for C being non empty compact Subset of () holds N-bound (L~ ()) = N-bound C
proof end;

theorem Th61: :: SPRECT_1:61
for C being non empty compact Subset of () holds E-bound (L~ ()) = E-bound C
proof end;

theorem Th62: :: SPRECT_1:62
for C being non empty compact Subset of () holds NW-corner (L~ ()) = NW-corner C
proof end;

theorem Th63: :: SPRECT_1:63
for C being non empty compact Subset of () holds NE-corner (L~ ()) = NE-corner C
proof end;

theorem Th64: :: SPRECT_1:64
for C being non empty compact Subset of () holds SW-corner (L~ ()) = SW-corner C
proof end;

theorem Th65: :: SPRECT_1:65
for C being non empty compact Subset of () holds SE-corner (L~ ()) = SE-corner C
proof end;

theorem Th66: :: SPRECT_1:66
for C being non empty compact Subset of () holds W-most (L~ ()) = LSeg ((),())
proof end;

theorem Th67: :: SPRECT_1:67
for C being non empty compact Subset of () holds N-most (L~ ()) = LSeg ((),())
proof end;

theorem Th68: :: SPRECT_1:68
for C being non empty compact Subset of () holds S-most (L~ ()) = LSeg ((),())
proof end;

theorem Th69: :: SPRECT_1:69
for C being non empty compact Subset of () holds E-most (L~ ()) = LSeg ((),())
proof end;

theorem Th70: :: SPRECT_1:70
for C being non empty compact Subset of () holds proj2 .: (LSeg ((),())) = [.(),().]
proof end;

theorem Th71: :: SPRECT_1:71
for C being non empty compact Subset of () holds proj1 .: (LSeg ((),())) = [.(),().]
proof end;

theorem Th72: :: SPRECT_1:72
for C being non empty compact Subset of () holds proj2 .: (LSeg ((),())) = [.(),().]
proof end;

theorem Th73: :: SPRECT_1:73
for C being non empty compact Subset of () holds proj1 .: (LSeg ((),())) = [.(),().]
proof end;

theorem Th74: :: SPRECT_1:74
for C being non empty compact Subset of () holds W-min (L~ ()) = SW-corner C
proof end;

theorem Th75: :: SPRECT_1:75
for C being non empty compact Subset of () holds W-max (L~ ()) = NW-corner C
proof end;

theorem Th76: :: SPRECT_1:76
for C being non empty compact Subset of () holds N-min (L~ ()) = NW-corner C
proof end;

theorem Th77: :: SPRECT_1:77
for C being non empty compact Subset of () holds N-max (L~ ()) = NE-corner C
proof end;

theorem Th78: :: SPRECT_1:78
for C being non empty compact Subset of () holds E-min (L~ ()) = SE-corner C
proof end;

theorem Th79: :: SPRECT_1:79
for C being non empty compact Subset of () holds E-max (L~ ()) = NE-corner C
proof end;

theorem Th80: :: SPRECT_1:80
for C being non empty compact Subset of () holds S-min (L~ ()) = SW-corner C
proof end;

theorem Th81: :: SPRECT_1:81
for C being non empty compact Subset of () holds S-max (L~ ()) = SE-corner C
proof end;

definition
let f be FinSequence of ();
attr f is rectangular means :Def2: :: SPRECT_1:def 2
ex D being non empty compact non horizontal non vertical Subset of () st f = SpStSeq D;
end;

:: deftheorem Def2 defines rectangular SPRECT_1:def 2 :
for f being FinSequence of () holds
( f is rectangular iff ex D being non empty compact non horizontal non vertical Subset of () st f = SpStSeq D );

registration
let D be non empty compact non horizontal non vertical Subset of ();
coherence ;
end;

registration
cluster V1() V4( NAT ) V5( the carrier of ()) Function-like V35() FinSequence-like FinSubsequence-like rectangular for FinSequence of the carrier of ();
existence
ex b1 being FinSequence of () st b1 is rectangular
proof end;
end;

theorem :: SPRECT_1:82
for s being rectangular FinSequence of () holds len s = 5
proof end;

registration
cluster rectangular -> non constant for FinSequence of the carrier of ();
coherence
for b1 being FinSequence of () st b1 is rectangular holds
not b1 is constant
;
end;

registration
cluster non empty rectangular -> non empty circular special unfolded s.c.c. standard for FinSequence of the carrier of ();
coherence
for b1 being non empty FinSequence of () st b1 is rectangular holds
( b1 is standard & b1 is special & b1 is unfolded & b1 is circular & b1 is s.c.c. )
;
end;

:: Special points of L~f, f - rectangular
theorem :: SPRECT_1:83
for s being rectangular FinSequence of () holds
( s /. 1 = N-min (L~ s) & s /. 1 = W-max (L~ s) )
proof end;

theorem :: SPRECT_1:84
for s being rectangular FinSequence of () holds
( s /. 2 = N-max (L~ s) & s /. 2 = E-max (L~ s) )
proof end;

theorem :: SPRECT_1:85
for s being rectangular FinSequence of () holds
( s /. 3 = S-max (L~ s) & s /. 3 = E-min (L~ s) )
proof end;

theorem :: SPRECT_1:86
for s being rectangular FinSequence of () holds
( s /. 4 = S-min (L~ s) & s /. 4 = W-min (L~ s) )
proof end;

theorem Th87: :: SPRECT_1:87
for r1, r2, s1, s2 being Real st r1 < r2 & s1 < s2 holds
[.r1,r2,s1,s2.] is Jordan
proof end;

registration
let f be rectangular FinSequence of ();
cluster L~ f -> Jordan ;
coherence
L~ f is Jordan
proof end;
end;

definition
let S be Subset of ();
redefine attr S is Jordan means :Def3: :: SPRECT_1:def 3
( S  <> {} & ex A1, A2 being Subset of () 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  ) );
compatibility
( S is Jordan iff ( S  <> {} & ex A1, A2 being Subset of () 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  ) ) )
proof end;
end;

:: deftheorem Def3 defines Jordan SPRECT_1:def 3 :
for S being Subset of () holds
( S is Jordan iff ( S  <> {} & ex A1, A2 being Subset of () 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  ) ) );

theorem Th88: :: SPRECT_1:88
for f being rectangular FinSequence of () holds LeftComp f misses RightComp f
proof end;

registration
let f be non constant standard special_circular_sequence;
cluster LeftComp f -> non empty ;
coherence
not LeftComp f is empty
proof end;
cluster RightComp f -> non empty ;
coherence
not RightComp f is empty
proof end;
end;

theorem :: SPRECT_1:89
for f being rectangular FinSequence of () holds LeftComp f <> RightComp f
proof end;