:: Upper and Lower Sequence of a Cage
:: by Robert Milewski
::
:: Received August 8, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users
begin
theorem
Th1
:
:: JORDAN1E:1
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is_in_the_area_of
g
holds
for
p
being
Element
of
(
TOP-REAL
2
)
st
p
in
rng
f
holds
f
-:
p
is_in_the_area_of
g
proof
end;
theorem
Th2
:
:: JORDAN1E:2
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is_in_the_area_of
g
holds
for
p
being
Element
of
(
TOP-REAL
2
)
st
p
in
rng
f
holds
f
:-
p
is_in_the_area_of
g
proof
end;
theorem
:: JORDAN1E:3
for
f
being
FinSequence
of
(
TOP-REAL
2
)
for
p
being
Point
of
(
TOP-REAL
2
)
st
p
in
L~
f
holds
L_Cut
(
f
,
p
)
<>
{}
proof
end;
theorem
:: JORDAN1E:4
for
f
being
FinSequence
of
(
TOP-REAL
2
)
for
p
being
Point
of
(
TOP-REAL
2
)
st
p
in
L~
f
&
len
(
R_Cut
(
f
,
p
)
)
>=
2 holds
f
.
1
in
L~
(
R_Cut
(
f
,
p
)
)
proof
end;
theorem
Th5
:
:: JORDAN1E:5
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
being_S-Seq
holds
for
p
being
Point
of
(
TOP-REAL
2
)
st
p
in
L~
f
holds
not
f
.
1
in
L~
(
mid
(
f
,
(
(
Index
(
p
,
f
)
)
+
1
)
,
(
len
f
)
)
)
proof
end;
theorem
Th6
:
:: JORDAN1E:6
for
i
,
j
,
m
,
n
being
Element
of
NAT
st
i
+
j
=
m
+
n
&
i
<=
m
&
j
<=
n
holds
i
=
m
proof
end;
theorem
:: JORDAN1E:7
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
being_S-Seq
holds
for
p
being
Point
of
(
TOP-REAL
2
)
st
p
in
L~
f
&
f
.
1
in
L~
(
L_Cut
(
f
,
p
)
)
holds
f
.
1
=
p
proof
end;
begin
definition
let
C
be
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
;
let
n
be
Nat
;
func
Upper_Seq
(
C
,
n
)
->
FinSequence
of
(
TOP-REAL
2
)
equals
:: JORDAN1E:def 1
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
-:
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
;
coherence
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
-:
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
is
FinSequence
of
(
TOP-REAL
2
)
;
end;
::
deftheorem
defines
Upper_Seq
JORDAN1E:def 1 :
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Nat
holds
Upper_Seq
(
C
,
n
)
=
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
-:
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
;
theorem
Th8
:
:: JORDAN1E:8
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Nat
holds
len
(
Upper_Seq
(
C
,
n
)
)
=
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
..
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
proof
end;
definition
let
C
be
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
;
let
n
be
Nat
;
func
Lower_Seq
(
C
,
n
)
->
FinSequence
of
(
TOP-REAL
2
)
equals
:: JORDAN1E:def 2
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
:-
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
;
coherence
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
:-
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
is
FinSequence
of
(
TOP-REAL
2
)
;
end;
::
deftheorem
defines
Lower_Seq
JORDAN1E:def 2 :
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Nat
holds
Lower_Seq
(
C
,
n
)
=
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
:-
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
;
theorem
Th9
:
:: JORDAN1E:9
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Nat
holds
len
(
Lower_Seq
(
C
,
n
)
)
=
(
(
len
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
)
-
(
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
..
(
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
)
)
)
+
1
proof
end;
registration
let
C
be
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
;
let
n
be
Nat
;
cluster
Upper_Seq
(
C
,
n
)
->
non
empty
;
coherence
not
Upper_Seq
(
C
,
n
) is
empty
proof
end;
cluster
Lower_Seq
(
C
,
n
)
->
non
empty
;
coherence
not
Lower_Seq
(
C
,
n
) is
empty
proof
end;
end;
registration
let
C
be
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
;
let
n
be
Element
of
NAT
;
cluster
Upper_Seq
(
C
,
n
)
->
one-to-one
special
unfolded
s.n.c.
;
coherence
(
Upper_Seq
(
C
,
n
) is
one-to-one
&
Upper_Seq
(
C
,
n
) is
special
&
Upper_Seq
(
C
,
n
) is
unfolded
&
Upper_Seq
(
C
,
n
) is
s.n.c.
)
proof
end;
cluster
Lower_Seq
(
C
,
n
)
->
one-to-one
special
unfolded
s.n.c.
;
coherence
(
Lower_Seq
(
C
,
n
) is
one-to-one
&
Lower_Seq
(
C
,
n
) is
special
&
Lower_Seq
(
C
,
n
) is
unfolded
&
Lower_Seq
(
C
,
n
) is
s.n.c.
)
proof
end;
end;
theorem
Th10
:
:: JORDAN1E:10
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Element
of
NAT
holds
(
len
(
Upper_Seq
(
C
,
n
)
)
)
+
(
len
(
Lower_Seq
(
C
,
n
)
)
)
=
(
len
(
Cage
(
C
,
n
)
)
)
+
1
proof
end;
theorem
Th11
:
:: JORDAN1E:11
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Element
of
NAT
holds
Rotate
(
(
Cage
(
C
,
n
)
)
,
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
)
=
(
Upper_Seq
(
C
,
n
)
)
^'
(
Lower_Seq
(
C
,
n
)
)
proof
end;
theorem
:: JORDAN1E:12
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Element
of
NAT
holds
L~
(
Cage
(
C
,
n
)
)
=
L~
(
(
Upper_Seq
(
C
,
n
)
)
^'
(
Lower_Seq
(
C
,
n
)
)
)
proof
end;
theorem
:: JORDAN1E:13
for
C
being non
empty
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Element
of
NAT
holds
L~
(
Cage
(
C
,
n
)
)
=
(
L~
(
Upper_Seq
(
C
,
n
)
)
)
\/
(
L~
(
Lower_Seq
(
C
,
n
)
)
)
proof
end;
theorem
Th14
:
:: JORDAN1E:14
for
P
being
Simple_closed_curve
holds
W-min
P
<>
E-min
P
proof
end;
theorem
Th15
:
:: JORDAN1E:15
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Element
of
NAT
holds
(
len
(
Upper_Seq
(
C
,
n
)
)
>=
3 &
len
(
Lower_Seq
(
C
,
n
)
)
>=
3 )
proof
end;
registration
let
C
be
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
;
let
n
be
Element
of
NAT
;
cluster
Upper_Seq
(
C
,
n
)
->
being_S-Seq
;
coherence
Upper_Seq
(
C
,
n
) is
being_S-Seq
proof
end;
cluster
Lower_Seq
(
C
,
n
)
->
being_S-Seq
;
coherence
Lower_Seq
(
C
,
n
) is
being_S-Seq
proof
end;
end;
theorem
:: JORDAN1E:16
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
n
being
Element
of
NAT
holds
(
L~
(
Upper_Seq
(
C
,
n
)
)
)
/\
(
L~
(
Lower_Seq
(
C
,
n
)
)
)
=
{
(
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
)
,
(
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
)
}
proof
end;
theorem
:: JORDAN1E:17
for
n
being
Element
of
NAT
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
holds
Upper_Seq
(
C
,
n
)
is_in_the_area_of
Cage
(
C
,
n
)
proof
end;
theorem
:: JORDAN1E:18
for
n
being
Element
of
NAT
for
C
being
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
holds
Lower_Seq
(
C
,
n
)
is_in_the_area_of
Cage
(
C
,
n
)
proof
end;
theorem
:: JORDAN1E:19
for
n
being
Element
of
NAT
for
C
being
connected
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
holds
(
(
Cage
(
C
,
n
)
)
/.
2
)
`2
=
N-bound
(
L~
(
Cage
(
C
,
n
)
)
)
proof
end;
theorem
:: JORDAN1E:20
for
n
being
Element
of
NAT
for
C
being
connected
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
k
being
Element
of
NAT
st 1
<=
k
&
k
+
1
<=
len
(
Cage
(
C
,
n
)
)
&
(
Cage
(
C
,
n
)
)
/.
k
=
E-max
(
L~
(
Cage
(
C
,
n
)
)
)
holds
(
(
Cage
(
C
,
n
)
)
/.
(
k
+
1
)
)
`1
=
E-bound
(
L~
(
Cage
(
C
,
n
)
)
)
proof
end;
theorem
:: JORDAN1E:21
for
n
being
Element
of
NAT
for
C
being
connected
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
k
being
Element
of
NAT
st 1
<=
k
&
k
+
1
<=
len
(
Cage
(
C
,
n
)
)
&
(
Cage
(
C
,
n
)
)
/.
k
=
S-max
(
L~
(
Cage
(
C
,
n
)
)
)
holds
(
(
Cage
(
C
,
n
)
)
/.
(
k
+
1
)
)
`2
=
S-bound
(
L~
(
Cage
(
C
,
n
)
)
)
proof
end;
theorem
:: JORDAN1E:22
for
n
being
Element
of
NAT
for
C
being
connected
compact
non
horizontal
non
vertical
Subset
of
(
TOP-REAL
2
)
for
k
being
Element
of
NAT
st 1
<=
k
&
k
+
1
<=
len
(
Cage
(
C
,
n
)
)
&
(
Cage
(
C
,
n
)
)
/.
k
=
W-min
(
L~
(
Cage
(
C
,
n
)
)
)
holds
(
(
Cage
(
C
,
n
)
)
/.
(
k
+
1
)
)
`1
=
W-bound
(
L~
(
Cage
(
C
,
n
)
)
)
proof
end;