:: SPPOL_1 semantic presentation

theorem :: SPPOL_1:1

canceled;

theorem :: SPPOL_1:2

canceled;

theorem :: SPPOL_1:3

canceled;

theorem :: SPPOL_1:4

canceled;

theorem :: SPPOL_1:5

for r, s being real number st r <= s holds
( r - 1 <= s & r - 1 < s & r <= s + 1 & r < s + 1 ) by XREAL_1:147, XREAL_1:149;

theorem :: SPPOL_1:6

for n, k being Nat st n < k holds
n <= k - 1

proof end;

theorem :: SPPOL_1:7

for k, m, n being Nat st 1 <= k - m & k - m <= n holds
( k - m in Seg n & k - m is Nat )

proof end;

Lm1: for r1, r2, s1, s2 being real number st r1 >= 0 & r2 >= 0 & s1 >= 0 & s2 >= 0 & (r1 * s1) + (r2 * s2) = 0 holds
( ( r1 = 0 or s1 = 0 ) & ( r2 = 0 or s2 = 0 ) )
by XREAL_1:73;

theorem :: SPPOL_1:8

canceled;

theorem :: SPPOL_1:9

canceled;

theorem :: SPPOL_1:10

canceled;

theorem :: SPPOL_1:11

canceled;

theorem Th12: :: SPPOL_1:12

for r, s1, s2 being real number st 0 <= r & r <= 1 & s1 >= 0 & s2 >= 0 & (r * s1) + ((1 - r) * s2) = 0 & not ( r = 0 & s2 = 0 ) & not ( r = 1 & s1 = 0 ) holds
( s1 = 0 & s2 = 0 )

proof end;

theorem Th13: :: SPPOL_1:13

for r, r1, r2 being real number st r < r1 & r < r2 holds
r < min r1,r2

proof end;

theorem Th14: :: SPPOL_1:14

for r, r1, r2 being real number st r > r1 & r > r2 holds
r > max r1,r2

proof end;

scheme :: SPPOL_1:sch 1
FinSeqFam{ F₁() -> non empty set , F₂() -> FinSequence of F₁(), F₃( FinSequence of F₁(), Nat) -> set , P₁[ Nat] } :

{ F₃(F₂(),i) where i is Nat : ( i in dom F₂() & P₁[i] ) } is finite

proof end;

scheme :: SPPOL_1:sch 2
FinSeqFam'{ F₁() -> non empty set , F₂() -> FinSequence of F₁(), F₃( FinSequence of F₁(), Nat) -> set , P₁[ Nat] } :

{ F₃(F₂(),i) where i is Nat : ( 1 <= i & i <= len F₂() & P₁[i] ) } is finite

proof end;

theorem Th15: :: SPPOL_1:15

for n being Nat
for x1, x2, x3 being Element of REAL n holds |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).|

proof end;

theorem :: SPPOL_1:16

for n being Nat
for x1, x2, x3 being Element of REAL n holds |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).|

proof end;

theorem Th17: :: SPPOL_1:17

for n being Nat
for p being Point of (TOP-REAL n) holds
( p is Element of REAL n & p is Point of (Euclid n) ) by EUCLID:25;

theorem :: SPPOL_1:18

for n being Nat
for up being Point of (Euclid n) holds
( up is Element of REAL n & up is Point of (TOP-REAL n) ) by EUCLID:25;

theorem :: SPPOL_1:19

for n being Nat
for x being Element of REAL n holds
( x is Point of (Euclid n) & x is Point of (TOP-REAL n) ) by EUCLID:25;

theorem Th20: :: SPPOL_1:20

for n being Nat
for u1, u2 being Point of (Euclid n)
for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds
dist u1,u2 = |.(v1 - v2).|

proof end;

theorem Th21: :: SPPOL_1:21

for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg p1,p2 holds
ex r being Real st
( 0 <= r & r <= 1 & p = ((1 - r) * p1) + (r * p2) )

proof end;

theorem :: SPPOL_1:22

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r being Real st 0 <= r & r <= 1 holds
((1 - r) * p1) + (r * p2) in LSeg p1,p2 ;

theorem :: SPPOL_1:23

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg p1,p2 holds
ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) )

proof end;

theorem Th24: :: SPPOL_1:24

for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg q1,q2 c= LSeg p1,p2 & p1 in LSeg q1,q2 & not p1 = q1 holds
p1 = q2

proof end;

theorem :: SPPOL_1:25

for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) holds
( not LSeg p1,p2 = LSeg q1,q2 or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )

proof end;

theorem :: SPPOL_1:26

for n being Nat holds TOP-REAL n is_T2 ;

theorem :: SPPOL_1:27

for n being Nat
for p being Point of (TOP-REAL n) holds {p} is closed by PCOMPS_1:10;

theorem Th28: :: SPPOL_1:28

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds LSeg p1,p2 is compact

proof end;

theorem Th29: :: SPPOL_1:29

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds LSeg p1,p2 is closed

proof end;

definition

let n be Nat;
let p be Point of (TOP-REAL n);
let P be Subset of (TOP-REAL n);
pred p is_extremal_in P means :Def1: :: SPPOL_1:def 1
( p in P & ( for p1, p2 being Point of (TOP-REAL n) st p in LSeg p1,p2 & LSeg p1,p2 c= P & not p = p1 holds
p = p2 ) );

end;

:: deftheorem Def1 defines is_extremal_in SPPOL_1:def 1 :

theorem :: SPPOL_1:30

for n being Nat
for p being Point of (TOP-REAL n)
for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds
p is_extremal_in Q

proof end;

theorem :: SPPOL_1:31

for n being Nat
for p being Point of (TOP-REAL n) holds p is_extremal_in {p}

proof end;

theorem Th32: :: SPPOL_1:32

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds p1 is_extremal_in LSeg p1,p2

proof end;

theorem :: SPPOL_1:33

for n being Nat
for p2, p1 being Point of (TOP-REAL n) holds p2 is_extremal_in LSeg p1,p2 by Th32;

theorem :: SPPOL_1:34

for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) holds
( not p is_extremal_in LSeg p1,p2 or p = p1 or p = p2 )

proof end;

theorem Th35: :: SPPOL_1:35

for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <> p2 `1 & p1 `2 <> p2 `2 holds
ex p being Point of (TOP-REAL 2) st
( p in LSeg p1,p2 & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )

proof end;

definition

let P be Subset of (TOP-REAL 2);
attr P is horizontal means :Def2: :: SPPOL_1:def 2
for p, q being Point of (TOP-REAL 2) st p in P & q in P holds
p `2 = q `2 ;
attr P is vertical means :Def3: :: SPPOL_1:def 3
for p, q being Point of (TOP-REAL 2) st p in P & q in P holds
p `1 = q `1 ;

end;

:: deftheorem Def2 defines horizontal SPPOL_1:def 2 :

:: deftheorem Def3 defines vertical SPPOL_1:def 3 :

Lm2: for P being Subset of (TOP-REAL 2) st not P is trivial & P is horizontal holds
not P is vertical

proof end;

registration

cluster non trivial horizontal -> non vertical Element of K40(the carrier of (TOP-REAL 2));
coherence by Lm2;
cluster non trivial vertical -> non horizontal Element of K40(the carrier of (TOP-REAL 2));
coherence by Lm2;

end;

theorem Th36: :: SPPOL_1:36

for p, q being Point of (TOP-REAL 2) holds
( p `2 = q `2 iff LSeg p,q is horizontal )

proof end;

theorem Th37: :: SPPOL_1:37

for p, q being Point of (TOP-REAL 2) holds
( p `1 = q `1 iff LSeg p,q is vertical )

proof end;

theorem :: SPPOL_1:38

for p1, p, q, p2 being Point of (TOP-REAL 2) st p1 in LSeg p,q & p2 in LSeg p,q & p1 `1 <> p2 `1 & p1 `2 = p2 `2 holds
LSeg p,q is horizontal

proof end;

theorem :: SPPOL_1:39

for p1, p, q, p2 being Point of (TOP-REAL 2) st p1 in LSeg p,q & p2 in LSeg p,q & p1 `2 <> p2 `2 & p1 `1 = p2 `1 holds
LSeg p,q is vertical

proof end;

theorem Th40: :: SPPOL_1:40

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) holds LSeg f,i is closed

proof end;

theorem Th41: :: SPPOL_1:41

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) holds
( not f is special or LSeg f,i is vertical or LSeg f,i is horizontal )

proof end;

theorem Th42: :: SPPOL_1:42

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f holds
not LSeg f,i is trivial

proof end;

theorem :: SPPOL_1:43

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f & LSeg f,i is vertical holds
not LSeg f,i is horizontal

proof end;

theorem Th44: :: SPPOL_1:44

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg f,i) where i is Nat : ( 1 <= i & i <= len f ) } is finite

proof end;

theorem Th45: :: SPPOL_1:45

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg f,i) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is finite

proof end;

Lm3: for f being FinSequence of the carrier of (TOP-REAL 2)
for k being Nat holds { (LSeg f,i) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite

proof end;

theorem :: SPPOL_1:46

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg f,i) where i is Nat : ( 1 <= i & i <= len f ) } is Subset-Family of (TOP-REAL 2)

proof end;

theorem Th47: :: SPPOL_1:47

for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg f,i) where i is Nat : ( 1 <= i & i + 1 <= len f ) } is Subset-Family of (TOP-REAL 2)

proof end;

Lm4: for f being FinSequence of the carrier of (TOP-REAL 2)
for k being Nat holds { (LSeg f,i) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2)

proof end;

theorem Th48: :: SPPOL_1:48

for Q being Subset of (TOP-REAL 2)
for f being FinSequence of the carrier of (TOP-REAL 2) st Q = union { (LSeg f,i) where i is Nat : ( 1 <= i & i + 1 <= len f ) } holds
Q is closed

proof end;

theorem :: SPPOL_1:49

for f being FinSequence of the carrier of (TOP-REAL 2) holds L~ f is closed by Th48;

Lm5: for f being FinSequence of the carrier of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for k being Nat st Q = union { (LSeg f,i) where i is Nat : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds
Q is closed

proof end;

definition

let IT be FinSequence of (TOP-REAL 2);
attr IT is alternating means :Def4: :: SPPOL_1:def 4
for i being Nat st 1 <= i & i + 2 <= len IT holds
( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 );

end;

:: deftheorem Def4 defines alternating SPPOL_1:def 4 :

theorem Th50: :: SPPOL_1:50

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 holds
(f /. (i + 1)) `2 = (f /. (i + 2)) `2

proof end;

theorem Th51: :: SPPOL_1:51

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `2 = (f /. (i + 1)) `2 holds
(f /. (i + 1)) `1 = (f /. (i + 2)) `1

proof end;

theorem Th52: :: SPPOL_1:52

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds
( p1 `2 = p2 `2 & p3 `2 <> p2 `2 )

proof end;

theorem :: SPPOL_1:53

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds
( p2 `2 = p3 `2 & p1 `2 <> p2 `2 )

proof end;

Lm6: for f being FinSequence of the carrier of (TOP-REAL 2)
for i being Nat
for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds
ex p being Point of (TOP-REAL 2) st
( p in LSeg p1,p2 & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )

proof end;

theorem :: SPPOL_1:54

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds
not LSeg (f /. i),(f /. (i + 2)) c= (LSeg f,i) \/ (LSeg f,(i + 1))

proof end;

theorem Th55: :: SPPOL_1:55

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg f,i is vertical holds
LSeg f,(i + 1) is horizontal

proof end;

theorem Th56: :: SPPOL_1:56

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg f,i is horizontal holds
LSeg f,(i + 1) is vertical

proof end;

theorem :: SPPOL_1:57

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg f,i is vertical & LSeg f,(i + 1) is horizontal ) holds
( LSeg f,i is horizontal & LSeg f,(i + 1) is vertical )

proof end;

theorem Th58: :: SPPOL_1:58

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg p,q & LSeg p,q c= (LSeg f,i) \/ (LSeg f,(i + 1)) & not f /. (i + 1) = p holds
f /. (i + 1) = q

proof end;

theorem Th59: :: SPPOL_1:59

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds
f /. (i + 1) is_extremal_in (LSeg f,i) \/ (LSeg f,(i + 1))

proof end;

theorem Th60: :: SPPOL_1:60

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2)
for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg p,q & f /. (i + 1) <> q & not p in (LSeg f,i) \/ (LSeg f,(i + 1)) holds
for s being Real st s > 0 holds
ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg f,i) \/ (LSeg f,(i + 1)) & p3 in LSeg p,q & p3 in Ball u,s )

proof end;

definition

let f1, f2 be FinSequence of the carrier of (TOP-REAL 2);
let P be Subset of (TOP-REAL 2);
pred f1,f2 are_generators_of P means :Def5: :: SPPOL_1:def 5
( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) );

end;

:: deftheorem Def5 defines are_generators_of SPPOL_1:def 5 :

theorem :: SPPOL_1:61

for i being Nat
for P being Subset of (TOP-REAL 2)
for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds
f1 /. i is_extremal_in P

proof end;