:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received November 30, 1997

:: Copyright (c) 1997-2017 Association of Mizar Users

registration

ex b_{1} being FinSequence st

( not b_{1} is empty & b_{1} is constant )
end;

cluster V1() V4( NAT ) non empty Function-like constant V35() FinSequence-like FinSubsequence-like for set ;

existence ex b

( not b

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 <> {}

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 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

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}

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;

registration

let n be Nat;

let f be non trivial FinSequence of (TOP-REAL n);

coherence

not L~ f is empty

end;
let f be non trivial FinSequence of (TOP-REAL n);

coherence

not L~ f is empty

proof end;

registration

coherence

( R^2-unit_square is special_polygonal & not R^2-unit_square is horizontal & not R^2-unit_square is vertical )

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

proof end;

registration

ex b_{1} being Subset of (TOP-REAL 2) st

( not b_{1} is vertical & not b_{1} is horizontal & not b_{1} is empty & b_{1} is compact )
end;

cluster non empty compact non horizontal non vertical for Element of bool the carrier of (TOP-REAL 2);

existence ex b

( not b

proof end;

theorem Th15: :: SPRECT_1:15

for C being non empty compact Subset of (TOP-REAL 2) holds

( C is vertical iff W-bound C = E-bound C )

( 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 (TOP-REAL 2) holds

( C is horizontal iff S-bound C = N-bound C )

( C is horizontal iff S-bound C = N-bound C )

proof end;

theorem :: SPRECT_1:17

for C being non empty compact Subset of (TOP-REAL 2) st NW-corner C = NE-corner C holds

C is vertical

C is vertical

proof end;

theorem :: SPRECT_1:18

for C being non empty compact Subset of (TOP-REAL 2) st SW-corner C = SE-corner C holds

C is vertical

C is vertical

proof end;

theorem :: SPRECT_1:19

for C being non empty compact Subset of (TOP-REAL 2) st NW-corner C = SW-corner C holds

C is horizontal

C is horizontal

proof end;

theorem :: SPRECT_1:20

for C being non empty compact Subset of (TOP-REAL 2) st NE-corner C = SE-corner C holds

C is horizontal

C is horizontal

proof end;

theorem Th23: :: SPRECT_1:23

for C being non empty compact Subset of (TOP-REAL 2) holds LSeg ((SE-corner C),(NE-corner C)) = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) holds LSeg ((SW-corner C),(SE-corner C)) = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) holds LSeg ((NW-corner C),(NE-corner C)) = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) holds LSeg ((SW-corner C),(NW-corner C)) = { p where p is Point of (TOP-REAL 2) : ( 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 (TOP-REAL 2) holds (LSeg ((SW-corner C),(NW-corner C))) /\ (LSeg ((NW-corner C),(NE-corner C))) = {(NW-corner C)}

proof end;

theorem Th28: :: SPRECT_1:28

for C being non empty compact Subset of (TOP-REAL 2) holds (LSeg ((NW-corner C),(NE-corner C))) /\ (LSeg ((NE-corner C),(SE-corner C))) = {(NE-corner C)}

proof end;

theorem Th29: :: SPRECT_1:29

for C being non empty compact Subset of (TOP-REAL 2) holds (LSeg ((SE-corner C),(NE-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) = {(SE-corner C)}

proof end;

theorem Th30: :: SPRECT_1:30

for C being non empty compact Subset of (TOP-REAL 2) holds (LSeg ((NW-corner C),(SW-corner C))) /\ (LSeg ((SW-corner C),(SE-corner C))) = {(SW-corner C)}

proof end;

theorem Th33: :: SPRECT_1:33

for D1 being non empty compact non vertical Subset of (TOP-REAL 2) holds LSeg ((SW-corner D1),(NW-corner D1)) misses LSeg ((SE-corner D1),(NE-corner D1))

proof end;

theorem Th34: :: SPRECT_1:34

for D2 being non empty compact non horizontal Subset of (TOP-REAL 2) holds LSeg ((SW-corner D2),(SE-corner D2)) misses LSeg ((NW-corner D2),(NE-corner D2))

proof end;

definition

let C be Subset of (TOP-REAL 2);

<*(NW-corner C),(NE-corner C),(SE-corner C)*> ^ <*(SW-corner C),(NW-corner C)*> is FinSequence of (TOP-REAL 2) ;

end;
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)*>;

coherence <*(NW-corner C),(NE-corner C),(SE-corner C)*> ^ <*(SW-corner C),(NW-corner C)*>;

<*(NW-corner C),(NE-corner C),(SE-corner C)*> ^ <*(SW-corner C),(NW-corner C)*> is FinSequence of (TOP-REAL 2) ;

:: deftheorem defines SpStSeq SPRECT_1:def 1 :

for C being Subset of (TOP-REAL 2) holds SpStSeq C = <*(NW-corner C),(NE-corner C),(SE-corner C)*> ^ <*(SW-corner C),(NW-corner C)*>;

for C being Subset of (TOP-REAL 2) holds SpStSeq C = <*(NW-corner C),(NE-corner C),(SE-corner C)*> ^ <*(SW-corner C),(NW-corner C)*>;

theorem Th41: :: SPRECT_1:41

for S being Subset of (TOP-REAL 2) holds 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))))

proof end;

registration

let D be non empty compact non vertical Subset of (TOP-REAL 2);

coherence

not SpStSeq D is constant

end;
coherence

not SpStSeq D is constant

proof end;

registration

let D be non empty compact non horizontal Subset of (TOP-REAL 2);

coherence

not SpStSeq D is constant

end;
coherence

not SpStSeq D is constant

proof end;

registration

let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);

coherence

( SpStSeq D is special & SpStSeq D is unfolded & SpStSeq D is circular & SpStSeq D is s.c.c. & SpStSeq D is standard )

end;
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;

theorem Th42: :: SPRECT_1:42

for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds L~ (SpStSeq D) = [.(W-bound D),(E-bound D),(S-bound D),(N-bound D).]

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

f .: X is bounded_above

end;
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;

theorem Th47: :: SPRECT_1:47

for S being Subset of (TOP-REAL 2)

for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds

W-bound S = min ((W-bound C1),(W-bound C2))

for C1, C2 being non empty compact Subset of (TOP-REAL 2) 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 (TOP-REAL 2)

for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds

S-bound S = min ((S-bound C1),(S-bound C2))

for C1, C2 being non empty compact Subset of (TOP-REAL 2) 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 (TOP-REAL 2)

for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds

N-bound S = max ((N-bound C1),(N-bound C2))

for C1, C2 being non empty compact Subset of (TOP-REAL 2) 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 (TOP-REAL 2)

for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds

E-bound S = max ((E-bound C1),(E-bound C2))

for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds

E-bound S = max ((E-bound C1),(E-bound C2))

proof end;

registration

let r1, r2 be Real;

coherence

for b_{1} being Subset of REAL st b_{1} = [.r1,r2.] holds

b_{1} is real-bounded

end;
coherence

for b

b

proof 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) ) )

( 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 (TOP-REAL 2) st p `1 <= q `1 holds

proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).]

proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).]

proof end;

theorem Th53: :: SPRECT_1:53

for p, q being Point of (TOP-REAL 2) st p `2 <= q `2 holds

proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).]

proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).]

proof end;

theorem Th66: :: SPRECT_1:66

for C being non empty compact Subset of (TOP-REAL 2) holds W-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(NW-corner C))

proof end;

theorem Th67: :: SPRECT_1:67

for C being non empty compact Subset of (TOP-REAL 2) holds N-most (L~ (SpStSeq C)) = LSeg ((NW-corner C),(NE-corner C))

proof end;

theorem Th68: :: SPRECT_1:68

for C being non empty compact Subset of (TOP-REAL 2) holds S-most (L~ (SpStSeq C)) = LSeg ((SW-corner C),(SE-corner C))

proof end;

theorem Th69: :: SPRECT_1:69

for C being non empty compact Subset of (TOP-REAL 2) holds E-most (L~ (SpStSeq C)) = LSeg ((SE-corner C),(NE-corner C))

proof end;

theorem Th70: :: SPRECT_1:70

for C being non empty compact Subset of (TOP-REAL 2) holds proj2 .: (LSeg ((SW-corner C),(NW-corner C))) = [.(S-bound C),(N-bound C).]

proof end;

theorem Th71: :: SPRECT_1:71

for C being non empty compact Subset of (TOP-REAL 2) holds proj1 .: (LSeg ((NW-corner C),(NE-corner C))) = [.(W-bound C),(E-bound C).]

proof end;

theorem Th72: :: SPRECT_1:72

for C being non empty compact Subset of (TOP-REAL 2) holds proj2 .: (LSeg ((NE-corner C),(SE-corner C))) = [.(S-bound C),(N-bound C).]

proof end;

theorem Th73: :: SPRECT_1:73

for C being non empty compact Subset of (TOP-REAL 2) holds proj1 .: (LSeg ((SE-corner C),(SW-corner C))) = [.(W-bound C),(E-bound C).]

proof end;

definition

let f be FinSequence of (TOP-REAL 2);

end;
attr f is rectangular means :Def2: :: SPRECT_1:def 2

ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D;

ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D;

:: deftheorem Def2 defines rectangular SPRECT_1:def 2 :

for f being FinSequence of (TOP-REAL 2) holds

( f is rectangular iff ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D );

for f being FinSequence of (TOP-REAL 2) holds

( f is rectangular iff ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D );

registration

let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);

coherence

SpStSeq D is rectangular ;

end;
coherence

SpStSeq D is rectangular ;

registration

ex b_{1} being FinSequence of (TOP-REAL 2) st b_{1} is rectangular
end;

cluster V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) Function-like V35() FinSequence-like FinSubsequence-like rectangular for FinSequence of the carrier of (TOP-REAL 2);

existence ex b

proof end;

registration

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} is rectangular holds

not b_{1} is constant
;

end;
for b

not b

registration

for b_{1} being non empty FinSequence of (TOP-REAL 2) st b_{1} is rectangular holds

( b_{1} is standard & b_{1} is special & b_{1} is unfolded & b_{1} is circular & b_{1} is s.c.c. )
;

end;

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

coherence for b

( b

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

theorem :: SPRECT_1:83

for s being rectangular FinSequence of (TOP-REAL 2) holds

( s /. 1 = N-min (L~ s) & s /. 1 = W-max (L~ s) )

( s /. 1 = N-min (L~ s) & s /. 1 = W-max (L~ s) )

proof end;

theorem :: SPRECT_1:84

for s being rectangular FinSequence of (TOP-REAL 2) holds

( s /. 2 = N-max (L~ s) & s /. 2 = E-max (L~ s) )

( s /. 2 = N-max (L~ s) & s /. 2 = E-max (L~ s) )

proof end;

theorem :: SPRECT_1:85

for s being rectangular FinSequence of (TOP-REAL 2) holds

( s /. 3 = S-max (L~ s) & s /. 3 = E-min (L~ s) )

( s /. 3 = S-max (L~ s) & s /. 3 = E-min (L~ s) )

proof end;

theorem :: SPRECT_1:86

for s being rectangular FinSequence of (TOP-REAL 2) holds

( s /. 4 = S-min (L~ s) & s /. 4 = W-min (L~ s) )

( s /. 4 = S-min (L~ s) & s /. 4 = W-min (L~ s) )

proof end;

registration
end;

definition

let S be Subset of (TOP-REAL 2);

( S is Jordan iff ( 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;
redefine attr S is Jordan means :Def3: :: 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 ` ) );

compatibility ( 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 ` ) );

( S is Jordan iff ( 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 ` ) ) )

proof end;

:: deftheorem Def3 defines Jordan SPRECT_1:def 3 :

for S being Subset of (TOP-REAL 2) holds

( S is Jordan iff ( 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 ` ) ) );

for S being Subset of (TOP-REAL 2) holds

( S is Jordan iff ( 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 ` ) ) );

registration

let f be non constant standard special_circular_sequence;

coherence

not LeftComp f is empty

not RightComp f is empty

end;
coherence

not LeftComp f is empty

proof end;

coherence not RightComp f is empty

proof end;