:: The Ordering of Points on a Curve, Part { I }
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Received September 10, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem Th1: :: JORDAN5B:1
for
i1 being
Nat st 1
<= i1 holds
i1 -' 1
< i1
theorem :: JORDAN5B:2
for
i,
k being
Nat st
i + 1
<= k holds
1
<= k -' i
theorem :: JORDAN5B:3
for
i,
k being
Nat st 1
<= i & 1
<= k holds
(k -' i) + 1
<= k
Lm1:
for r being real number st 0 <= r & r <= 1 holds
( 0 <= 1 - r & 1 - r <= 1 )
theorem :: JORDAN5B:4
theorem :: JORDAN5B:5
theorem :: JORDAN5B:6
Lm2:
for P being Point of I[01] holds P is Real
theorem Th7: :: JORDAN5B:7
theorem :: JORDAN5B:8
theorem Th9: :: JORDAN5B:9
theorem Th10: :: JORDAN5B:10
theorem Th11: :: JORDAN5B:11
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
theorem :: JORDAN5B:13
theorem :: JORDAN5B:14
theorem :: JORDAN5B:15
theorem :: JORDAN5B:16
theorem :: JORDAN5B:17
theorem :: JORDAN5B:18
canceled;
theorem :: JORDAN5B:19
canceled;
theorem :: JORDAN5B:20
canceled;
theorem :: JORDAN5B:21
theorem Th22: :: JORDAN5B:22
theorem :: JORDAN5B:23
theorem Th24: :: JORDAN5B:24
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) & q <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut f,q) holds
q in L~ (L_Cut f,p)
theorem Th25: :: JORDAN5B:25
theorem :: JORDAN5B:26
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
theorem :: JORDAN5B:27
theorem :: JORDAN5B:28
theorem :: JORDAN5B:29
theorem Th30: :: JORDAN5B:30
theorem :: JORDAN5B:31
theorem :: JORDAN5B:32
theorem :: JORDAN5B:33
theorem :: JORDAN5B:34
theorem :: JORDAN5B:35
theorem :: JORDAN5B:36
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 by Lm4;