:: by Adam Grabowski and Yatsuka Nakamura

::

:: Received September 10, 1997

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

begin

Lm1: for r being real number st 0 <= r & r <= 1 holds

( 0 <= 1 - r & 1 - r <= 1 )

proof end;

theorem :: JORDAN5B:5

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

p1 = p

p1 = p

proof end;

theorem :: JORDAN5B:6

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

p1 = p

p1 = p

proof end;

Lm2: for P being Point of I[01] holds P is Real

proof end;

theorem Th7: :: JORDAN5B:7

for f being FinSequence of (TOP-REAL 2)

for P being non empty Subset of (TOP-REAL 2)

for F being Function of I[01],((TOP-REAL 2) | P)

for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds

ex p1, p2 being Real st

( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) )

for P being non empty Subset of (TOP-REAL 2)

for F being Function of I[01],((TOP-REAL 2) | P)

for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds

ex p1, p2 being Real st

( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) )

proof end;

theorem :: JORDAN5B:8

for f being FinSequence of (TOP-REAL 2)

for Q, R being non empty Subset of (TOP-REAL 2)

for F being Function of I[01],((TOP-REAL 2) | Q)

for i being Element of NAT

for P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) holds

ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st

( G = F | P & G is being_homeomorphism )

for Q, R being non empty Subset of (TOP-REAL 2)

for F being Function of I[01],((TOP-REAL 2) | Q)

for i being Element of NAT

for P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) holds

ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st

( G = F | P & G is being_homeomorphism )

proof end;

begin

theorem :: JORDAN5B:12

for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2,p1,p2 & LE q2,q3,p1,p2 holds

LE q1,q3,p1,p2

LE q1,q3,p1,p2

proof end;

theorem :: JORDAN5B:13

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

LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) }

LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) }

proof end;

theorem :: JORDAN5B:14

for n being Element of NAT

for P being Subset of (TOP-REAL n)

for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds

P is_an_arc_of p2,p1

for P being Subset of (TOP-REAL n)

for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds

P is_an_arc_of p2,p1

proof end;

theorem :: JORDAN5B:15

for i being Element of NAT

for f being FinSequence of (TOP-REAL 2)

for P being Subset of (TOP-REAL 2) st f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg (f,i) holds

P is_an_arc_of f /. i,f /. (i + 1)

for f being FinSequence of (TOP-REAL 2)

for P being Subset of (TOP-REAL 2) st f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg (f,i) holds

P is_an_arc_of f /. i,f /. (i + 1)

proof end;

begin

theorem :: JORDAN5B:16

for g1 being FinSequence of (TOP-REAL 2)

for i being Element of NAT st 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) holds

i = 1

for i being Element of NAT st 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) holds

i = 1

proof end;

theorem :: JORDAN5B:17

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f . (len f) holds

L_Cut (f,p) = <*p*>

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f . (len f) holds

L_Cut (f,p) = <*p*>

proof end;

theorem :: JORDAN5B:18

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f & p <> f . (len f) & f is being_S-Seq holds

Index (p,(L_Cut (f,p))) = 1

for p being Point of (TOP-REAL 2) st p in L~ f & p <> f . (len f) & f is being_S-Seq holds

Index (p,(L_Cut (f,p))) = 1

proof end;

theorem Th19: :: JORDAN5B:19

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . (len f) holds

p in L~ (L_Cut (f,p))

for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . (len f) holds

p in L~ (L_Cut (f,p))

proof end;

theorem :: JORDAN5B:20

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . 1 holds

p in L~ (R_Cut (f,p))

for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . 1 holds

p in L~ (R_Cut (f,p))

proof end;

theorem Th21: :: JORDAN5B:21

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f & f is one-to-one holds

B_Cut (f,p,p) = <*p*>

for p being Point of (TOP-REAL 2) st p in L~ f & f is one-to-one holds

B_Cut (f,p,p) = <*p*>

proof end;

Lm3: for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds

q in L~ (L_Cut (f,p))

proof end;

theorem Th22: :: JORDAN5B:22

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq holds

p in L~ (L_Cut (f,q))

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq holds

p in L~ (L_Cut (f,q))

proof end;

theorem :: JORDAN5B:23

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p <> f . (len f) & p in L~ f & q in L~ f & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds

q in L~ (L_Cut (f,p))

for p, q being Point of (TOP-REAL 2) st p <> f . (len f) & p in L~ f & q in L~ f & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds

q in L~ (L_Cut (f,p))

proof end;

Lm4: for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) & p <> q holds

L~ (B_Cut (f,p,q)) c= L~ f

proof end;

theorem :: JORDAN5B:24

for f being FinSequence of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is being_S-Seq holds

L~ (B_Cut (f,p,q)) c= L~ f

for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is being_S-Seq holds

L~ (B_Cut (f,p,q)) c= L~ f

proof end;

theorem :: JORDAN5B:25

for f being non constant standard special_circular_sequence

for i, j being Element of NAT st 1 <= i & j <= len (GoB f) & i < j holds

(LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}

for i, j being Element of NAT st 1 <= i & j <= len (GoB f) & i < j holds

(LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}

proof end;

theorem :: JORDAN5B:26

for f being non constant standard special_circular_sequence

for i, j being Element of NAT st 1 <= i & j <= width (GoB f) & i < j holds

(LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}

for i, j being Element of NAT st 1 <= i & j <= width (GoB f) & i < j holds

(LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}

proof end;

theorem :: JORDAN5B:29

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))

for p being Point of (TOP-REAL 2) st p in L~ f holds

p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))

proof end;

theorem :: JORDAN5B:30

for f being FinSequence of (TOP-REAL 2)

for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) holds

i = 1

for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) holds

i = 1

proof end;

theorem :: JORDAN5B:31

for f being non constant standard special_circular_sequence

for j being Element of NAT

for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) holds

P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j)

for j being Element of NAT

for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) holds

P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j)

proof end;

theorem :: JORDAN5B:32

for f being non constant standard special_circular_sequence

for j being Element of NAT

for P being Subset of (TOP-REAL 2) st 1 <= j & j <= len (GoB f) & P = LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) holds

P is_S-P_arc_joining (GoB f) * (j,1),(GoB f) * (j,(width (GoB f)))

for j being Element of NAT

for P being Subset of (TOP-REAL 2) st 1 <= j & j <= len (GoB f) & P = LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) holds

P is_S-P_arc_joining (GoB f) * (j,1),(GoB f) * (j,(width (GoB f)))

proof end;

theorem :: JORDAN5B:33