begin
Lm1:
for a, b being real number st b <= 0 & a <= b holds
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
Lm2:
for a, b being real number st a <= 0 & a <= b holds
a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))
Lm3:
for a, b being real number st a >= 0 & a >= b holds
a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
begin
Lm4:
|[(- 1),0]| `1 = - 1
by EUCLID:56;
Lm5:
|[(- 1),0]| `2 = 0
by EUCLID:56;
Lm6:
|[1,0]| `1 = 1
by EUCLID:56;
Lm7:
|[1,0]| `2 = 0
by EUCLID:56;
Lm8:
|[0,(- 1)]| `1 = 0
by EUCLID:56;
Lm9:
|[0,(- 1)]| `2 = - 1
by EUCLID:56;
Lm10:
|[0,1]| `1 = 0
by EUCLID:56;
Lm11:
|[0,1]| `2 = 1
by EUCLID:56;
Lm12:
now
thus |.|[(- 1),0]|.| =
sqrt (((- 1) ^2) + (0 ^2))
by Lm4, Lm5, JGRAPH_3:10
.=
1
by SQUARE_1:83
;
( |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )thus |.|[1,0]|.| =
sqrt ((1 ^2) + (0 ^2))
by Lm6, Lm7, JGRAPH_3:10
.=
1
by SQUARE_1:83
;
( |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )thus |.|[0,(- 1)]|.| =
sqrt ((0 ^2) + ((- 1) ^2))
by Lm8, Lm9, JGRAPH_3:10
.=
1
by SQUARE_1:83
;
|.|[0,1]|.| = 1thus |.|[0,1]|.| =
sqrt ((0 ^2) + (1 ^2))
by Lm10, Lm11, JGRAPH_3:10
.=
1
by SQUARE_1:83
;
verum
end;
Lm13:
0 in [.0,1.]
by XXREAL_1:1;
Lm14:
1 in [.0,1.]
by XXREAL_1:1;
theorem
canceled;
theorem Th23:
theorem Th24:
theorem Th25:
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
C0 being
Subset of
(TOP-REAL 2) st
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } &
LE p1,
p2,
P &
LE p2,
p3,
P &
LE p3,
p4,
P holds
for
f,
g being
Function of
I[01],
(TOP-REAL 2) st
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } &
f . 0 = p3 &
f . 1
= p1 &
g . 0 = p2 &
g . 1
= p4 &
rng f c= C0 &
rng g c= C0 holds
rng f meets rng g
theorem Th26:
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
C0 being
Subset of
(TOP-REAL 2) st
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } &
LE p1,
p2,
P &
LE p2,
p3,
P &
LE p3,
p4,
P holds
for
f,
g being
Function of
I[01],
(TOP-REAL 2) st
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } &
f . 0 = p3 &
f . 1
= p1 &
g . 0 = p4 &
g . 1
= p2 &
rng f c= C0 &
rng g c= C0 holds
rng f meets rng g
theorem Th27:
begin
Lm15:
for a, b, c, d being real number st a <= b & c <= d holds
rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = a & c <= p `2 & p `2 <= d ) or ( p `2 = d & a <= p `1 & p `1 <= b ) or ( p `1 = b & c <= p `2 & p `2 <= d ) or ( p `2 = c & a <= p `1 & p `1 <= b ) ) }
theorem Th28:
:: deftheorem defines inside_of_rectangle JGRAPH_6:def 1 :
for a, b, c, d being real number holds inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } ;
:: deftheorem defines closed_inside_of_rectangle JGRAPH_6:def 2 :
for a, b, c, d being real number holds closed_inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } ;
:: deftheorem defines outside_of_rectangle JGRAPH_6:def 3 :
for a, b, c, d being real number holds outside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( not a <= p `1 or not p `1 <= b or not c <= p `2 or not p `2 <= d ) } ;
:: deftheorem defines closed_outside_of_rectangle JGRAPH_6:def 4 :
for a, b, c, d being real number holds closed_outside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( not a < p `1 or not p `1 < b or not c < p `2 or not p `2 < d ) } ;
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem defines circle JGRAPH_6:def 5 :
for a, b, r being real number holds circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ;
:: deftheorem defines inside_of_circle JGRAPH_6:def 6 :
for a, b, r being real number holds inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } ;
:: deftheorem defines closed_inside_of_circle JGRAPH_6:def 7 :
for a, b, r being real number holds closed_inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } ;
:: deftheorem defines outside_of_circle JGRAPH_6:def 8 :
for a, b, r being real number holds outside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } ;
:: deftheorem defines closed_outside_of_circle JGRAPH_6:def 9 :
for a, b, r being real number holds closed_outside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| >= r } ;
theorem Th33:
for
r being
real number holds
(
inside_of_circle (
0,
0,
r)
= { p where p is Point of (TOP-REAL 2) : |.p.| < r } & (
r > 0 implies
circle (
0,
0,
r)
= { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ) &
outside_of_circle (
0,
0,
r)
= { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } &
closed_inside_of_circle (
0,
0,
r)
= { q where q is Point of (TOP-REAL 2) : |.q.| <= r } &
closed_outside_of_circle (
0,
0,
r)
= { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
for
P0,
P1,
P01,
P11,
K0,
K1,
K01,
K11 being
Subset of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle (
0,
0,1) &
P0 = inside_of_circle (
0,
0,1) &
P1 = outside_of_circle (
0,
0,1) &
P01 = closed_inside_of_circle (
0,
0,1) &
P11 = closed_outside_of_circle (
0,
0,1) &
K0 = inside_of_rectangle (
(- 1),1,
(- 1),1) &
K1 = outside_of_rectangle (
(- 1),1,
(- 1),1) &
K01 = closed_inside_of_rectangle (
(- 1),1,
(- 1),1) &
K11 = closed_outside_of_rectangle (
(- 1),1,
(- 1),1) &
f = Sq_Circ holds
(
f .: (rectangle ((- 1),1,(- 1),1)) = P &
(f ") .: P = rectangle (
(- 1),1,
(- 1),1) &
f .: K0 = P0 &
(f ") .: P0 = K0 &
f .: K1 = P1 &
(f ") .: P1 = K1 &
f .: K01 = P01 &
f .: K11 = P11 &
(f ") .: P01 = K01 &
(f ") .: P11 = K11 )
begin
theorem Th39:
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(
LSeg (
|[a,c]|,
|[a,d]|)
= { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = a & p1 `2 <= d & p1 `2 >= c ) } &
LSeg (
|[a,d]|,
|[b,d]|)
= { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } &
LSeg (
|[a,c]|,
|[b,c]|)
= { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } &
LSeg (
|[b,c]|,
|[b,d]|)
= { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )
theorem
canceled;
theorem Th41:
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|}
theorem Th42:
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,c]|}
theorem Th43:
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(LSeg (|[a,d]|,|[b,d]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,d]|}
theorem Th44:
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,d]|,|[b,d]|)) = {|[a,d]|}
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem
theorem
theorem Th54:
theorem Th55:
theorem Th56:
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(
W-min (rectangle (a,b,c,d)) = |[a,c]| &
E-max (rectangle (a,b,c,d)) = |[b,d]| )
theorem Th57:
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
(
(LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) is_an_arc_of W-min (rectangle (a,b,c,d)),
E-max (rectangle (a,b,c,d)) &
(LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) is_an_arc_of E-max (rectangle (a,b,c,d)),
W-min (rectangle (a,b,c,d)) )
theorem Th58:
for
a,
b,
c,
d being
real number for
f1,
f2 being
FinSequence of
(TOP-REAL 2) for
p0,
p1,
p01,
p10 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p0 = |[a,c]| &
p1 = |[b,d]| &
p01 = |[a,d]| &
p10 = |[b,c]| &
f1 = <*p0,p01,p1*> &
f2 = <*p0,p10,p1*> holds
(
f1 is
being_S-Seq &
L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) &
f2 is
being_S-Seq &
L~ f2 = (LSeg (p0,p10)) \/ (LSeg (p10,p1)) &
rectangle (
a,
b,
c,
d)
= (L~ f1) \/ (L~ f2) &
(L~ f1) /\ (L~ f2) = {p0,p1} &
f1 /. 1
= p0 &
f1 /. (len f1) = p1 &
f2 /. 1
= p0 &
f2 /. (len f2) = p1 )
theorem Th59:
for
P1,
P2 being
Subset of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f1,
f2 being
FinSequence of
(TOP-REAL 2) for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 = |[a,c]| &
p2 = |[b,d]| &
f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> &
f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> &
P1 = L~ f1 &
P2 = L~ f2 holds
(
P1 is_an_arc_of p1,
p2 &
P2 is_an_arc_of p1,
p2 & not
P1 is
empty & not
P2 is
empty &
rectangle (
a,
b,
c,
d)
= P1 \/ P2 &
P1 /\ P2 = {p1,p2} )
theorem Th60:
theorem Th61:
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))
theorem Th62:
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))
theorem Th63:
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
ex
f being
Function of
I[01],
((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) st
(
f is
being_homeomorphism &
f . 0 = W-min (rectangle (a,b,c,d)) &
f . 1
= E-max (rectangle (a,b,c,d)) &
rng f = Upper_Arc (rectangle (a,b,c,d)) & ( for
r being
Real st
r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) ) & ( for
r being
Real st
r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg (
|[a,c]|,
|[a,d]|) holds
(
0 <= (((p `2) - c) / (d - c)) / 2 &
(((p `2) - c) / (d - c)) / 2
<= 1 &
f . ((((p `2) - c) / (d - c)) / 2) = p ) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg (
|[a,d]|,
|[b,d]|) holds
(
0 <= ((((p `1) - a) / (b - a)) / 2) + (1 / 2) &
((((p `1) - a) / (b - a)) / 2) + (1 / 2) <= 1 &
f . (((((p `1) - a) / (b - a)) / 2) + (1 / 2)) = p ) ) )
theorem Th64:
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
ex
f being
Function of
I[01],
((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) st
(
f is
being_homeomorphism &
f . 0 = E-max (rectangle (a,b,c,d)) &
f . 1
= W-min (rectangle (a,b,c,d)) &
rng f = Lower_Arc (rectangle (a,b,c,d)) & ( for
r being
Real st
r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[b,d]|) + ((2 * r) * |[b,c]|) ) & ( for
r being
Real st
r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[b,c]|) + (((2 * r) - 1) * |[a,c]|) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg (
|[b,d]|,
|[b,c]|) holds
(
0 <= (((p `2) - d) / (c - d)) / 2 &
(((p `2) - d) / (c - d)) / 2
<= 1 &
f . ((((p `2) - d) / (c - d)) / 2) = p ) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg (
|[b,c]|,
|[a,c]|) holds
(
0 <= ((((p `1) - b) / (a - b)) / 2) + (1 / 2) &
((((p `1) - b) / (a - b)) / 2) + (1 / 2) <= 1 &
f . (((((p `1) - b) / (a - b)) / 2) + (1 / 2)) = p ) ) )
theorem Th65:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg (
|[a,c]|,
|[a,d]|) &
p2 in LSeg (
|[a,c]|,
|[a,d]|) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) iff
p1 `2 <= p2 `2 )
theorem Th66:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg (
|[a,d]|,
|[b,d]|) &
p2 in LSeg (
|[a,d]|,
|[b,d]|) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) iff
p1 `1 <= p2 `1 )
theorem Th67:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg (
|[b,c]|,
|[b,d]|) &
p2 in LSeg (
|[b,c]|,
|[b,d]|) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) iff
p1 `2 >= p2 `2 )
theorem Th68:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg (
|[a,c]|,
|[b,c]|) &
p2 in LSeg (
|[a,c]|,
|[b,c]|) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) &
p1 <> W-min (rectangle (a,b,c,d)) iff (
p1 `1 >= p2 `1 &
p2 <> W-min (rectangle (a,b,c,d)) ) )
theorem Th69:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg (
|[a,c]|,
|[a,d]|) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) iff ( (
p2 in LSeg (
|[a,c]|,
|[a,d]|) &
p1 `2 <= p2 `2 ) or
p2 in LSeg (
|[a,d]|,
|[b,d]|) or
p2 in LSeg (
|[b,d]|,
|[b,c]|) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) ) )
theorem Th70:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg (
|[a,d]|,
|[b,d]|) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) iff ( (
p2 in LSeg (
|[a,d]|,
|[b,d]|) &
p1 `1 <= p2 `1 ) or
p2 in LSeg (
|[b,d]|,
|[b,c]|) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) ) )
theorem Th71:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg (
|[b,d]|,
|[b,c]|) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) iff ( (
p2 in LSeg (
|[b,d]|,
|[b,c]|) &
p1 `2 >= p2 `2 ) or (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p2 <> W-min (rectangle (a,b,c,d)) ) ) )
theorem Th72:
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg (
|[b,c]|,
|[a,c]|) &
p1 <> W-min (rectangle (a,b,c,d)) holds
(
LE p1,
p2,
rectangle (
a,
b,
c,
d) iff (
p2 in LSeg (
|[b,c]|,
|[a,c]|) &
p1 `1 >= p2 `1 &
p2 <> W-min (rectangle (a,b,c,d)) ) )
theorem Th73:
for
x being
set for
a,
b,
c,
d being
real number st
x in rectangle (
a,
b,
c,
d) &
a < b &
c < d & not
x in LSeg (
|[a,c]|,
|[a,d]|) & not
x in LSeg (
|[a,d]|,
|[b,d]|) & not
x in LSeg (
|[b,d]|,
|[b,c]|) holds
x in LSeg (
|[b,c]|,
|[a,c]|)
begin
theorem Th74:
for
p1,
p2 being
Point of
(TOP-REAL 2) st
LE p1,
p2,
rectangle (
(- 1),1,
(- 1),1) &
p1 in LSeg (
|[(- 1),(- 1)]|,
|[(- 1),1]|) & not (
p2 in LSeg (
|[(- 1),(- 1)]|,
|[(- 1),1]|) &
p2 `2 >= p1 `2 ) & not
p2 in LSeg (
|[(- 1),1]|,
|[1,1]|) & not
p2 in LSeg (
|[1,1]|,
|[1,(- 1)]|) holds
(
p2 in LSeg (
|[1,(- 1)]|,
|[(- 1),(- 1)]|) &
p2 <> |[(- 1),(- 1)]| )
theorem Th75:
for
p1,
p2 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle (
0,
0,1) &
f = Sq_Circ &
p1 in LSeg (
|[(- 1),(- 1)]|,
|[(- 1),1]|) &
p1 `2 >= 0 &
LE p1,
p2,
rectangle (
(- 1),1,
(- 1),1) holds
LE f . p1,
f . p2,
P
theorem Th76:
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle (
0,
0,1) &
f = Sq_Circ &
p1 in LSeg (
|[(- 1),(- 1)]|,
|[(- 1),1]|) &
p1 `2 >= 0 &
LE p1,
p2,
rectangle (
(- 1),1,
(- 1),1) &
LE p2,
p3,
rectangle (
(- 1),1,
(- 1),1) holds
LE f . p2,
f . p3,
P
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle (
0,
0,1) &
f = Sq_Circ &
LE p1,
p2,
rectangle (
(- 1),1,
(- 1),1) &
LE p2,
p3,
rectangle (
(- 1),1,
(- 1),1) &
LE p3,
p4,
rectangle (
(- 1),1,
(- 1),1) holds
f . p1,
f . p2,
f . p3,
f . p4 are_in_this_order_on P
theorem Th83:
theorem
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) st
P is
being_simple_closed_curve &
p1 in P &
p2 in P &
p3 in P & not (
LE p1,
p2,
P &
LE p2,
p3,
P ) & not (
LE p1,
p3,
P &
LE p3,
p2,
P ) & not (
LE p2,
p1,
P &
LE p1,
p3,
P ) & not (
LE p2,
p3,
P &
LE p3,
p1,
P ) & not (
LE p3,
p1,
P &
LE p1,
p2,
P ) holds
(
LE p3,
p2,
P &
LE p2,
p1,
P )
by Th83;
theorem
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) st
P is
being_simple_closed_curve &
p1 in P &
p2 in P &
p3 in P &
LE p2,
p3,
P & not
LE p1,
p2,
P & not (
LE p2,
p1,
P &
LE p1,
p3,
P ) holds
LE p3,
p1,
P by Th83;
theorem
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) st
P is
being_simple_closed_curve &
p1 in P &
p2 in P &
p3 in P &
p4 in P &
LE p2,
p3,
P &
LE p3,
p4,
P & not
LE p1,
p2,
P & not (
LE p2,
p1,
P &
LE p1,
p3,
P ) & not (
LE p3,
p1,
P &
LE p1,
p4,
P ) holds
LE p4,
p1,
P by Th83;
theorem Th87:
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle (
0,
0,1) &
f = Sq_Circ &
LE f . p1,
f . p2,
P &
LE f . p2,
f . p3,
P &
LE f . p3,
f . p4,
P holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1)
theorem Th88:
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle (
0,
0,1) &
f = Sq_Circ holds
(
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1) iff
f . p1,
f . p2,
f . p3,
f . p4 are_in_this_order_on P )
theorem
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) st
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1) holds
for
f,
g being
Function of
I[01],
(TOP-REAL 2) st
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
rng f c= closed_inside_of_rectangle (
(- 1),1,
(- 1),1) &
rng g c= closed_inside_of_rectangle (
(- 1),1,
(- 1),1) holds
rng f meets rng g