:: Jordan Curve Theorem
:: by Artur Korni{\l}owicz
::
:: Received September 15, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, TOPREAL2, RELAT_1, RCOMP_1,
JORDAN21, TARSKI, XBOOLE_0, RELAT_2, METRIC_1, XXREAL_0, CARD_1, ARYTM_3,
SUPINF_2, ARYTM_1, MCART_1, SPPOL_1, RLTOPSP1, PSCOMP_1, JORDAN6,
JORDAN2C, CONVEX1, TOPREAL1, STRUCT_0, TOPMETR, VALUED_1, TREAL_1,
ZFMISC_1, REAL_1, FUNCOP_1, ORDINAL2, COMPLEX1, BROUWER, TOPREALB,
XCMPLX_0, TOPS_1, PCOMPS_1, XXREAL_2, FUNCT_1, TOPS_2, FUNCT_2, GRAPH_1,
BORSUK_2, BORSUK_1, XXREAL_1, JGRAPH_6, JORDAN5C, JORDAN3, SQUARE_1,
PARTFUN3, PARTFUN1, TOPREALA, SETFAM_1, PROB_1, ABIAN, CONNSP_1,
CONNSP_2, TOPREAL4, FUNCT_4, TOPGRP_1, JORDAN24, CONNSP_3, JORDAN1,
JORDAN, MEASURE5, SEQ_4, NAT_1, FUNCT_7;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, SQUARE_1,
MCART_1, RELAT_1, VALUED_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
FUNCT_3, FUNCT_4, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2,
XREAL_0, COMPLEX1, REAL_1, RCOMP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1,
BORSUK_1, TOPS_2, COMPTS_1, TREAL_1, CONNSP_1, CONNSP_2, CONNSP_3,
METRIC_1, TBSP_1, RLVECT_1, PCOMPS_1, RLTOPSP1, EUCLID, BORSUK_2,
TOPREAL1, TOPREAL2, TOPMETR, SPPOL_1, JORDAN1, JORDAN2C, JORDAN5C,
TOPREAL4, JORDAN6, JGRAPH_6, TOPREAL6, TOPREAL9, BORSUK_6, TOPREALA,
JORDAN21, TOPGRP_1, JORDAN24, ABIAN, PARTFUN3, TOPREALB, BROUWER,
PSCOMP_1;
constructors FUNCT_4, SQUARE_1, COMPLEX1, ABIAN, TOPS_1, CONNSP_1, COMPTS_1,
TBSP_1, TSEP_1, TOPREAL1, TREAL_1, TOPREAL4, SPPOL_1, JORDAN1, SPPOL_2,
CONNSP_3, WAYBEL_3, JORDAN5C, JORDAN6, TOPGRP_1, JORDAN2C, TOPREAL6,
JORDAN21, JGRAPH_6, TOPREAL9, TOPREALA, PARTFUN3, BROUWER, JORDAN24,
BORSUK_6, SEQ_4, FUNCSDOM, CONVEX1, BINOP_2, PSCOMP_1, XTUPLE_0, REAL_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS,
XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1,
COMPTS_1, METRIC_1, BORSUK_1, TEX_2, EUCLID, TOPMETR, TOPREAL1, TOPREAL2,
SPPOL_1, JORDAN1, SPPOL_2, PSCOMP_1, BORSUK_2, WAYBEL_2, WAYBEL_3,
JORDAN5A, JORDAN6, TOPGRP_1, YELLOW13, JORDAN2C, TOPREAL6, JORDAN21,
TOPREAL9, TOPREALA, TOPREALB, RCOMP_3, PARTFUN3, TOPALG_5, BROUWER,
JGRAPH_8, VALUED_0, XXREAL_2, RELAT_1, MEASURE6, PARTFUN4, VALUED_1,
XTUPLE_0, ORDINAL1, CARD_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: Preliminaries
:: I would like to thank Professor Yatsuka Nakamura
:: for including me to the team working on the formalization
:: of the Jordan Curve Theorem. Especially, I am very grateful
:: to Professor Nakamura for inviting me to Shinshu University, Nagano
:: to work on the project together.
:: I am also thankful to Professor Andrzej Trybulec for his
:: continual help and fruitful discussions during the formalization.
reserve a, b, c, d, r, s for Real,
n for Element of NAT,
p, p1, p2 for Point of TOP-REAL 2,
x, y for Point of TOP-REAL n,
C for Simple_closed_curve,
A, B, P for Subset of TOP-REAL 2,
U, V for Subset of (TOP-REAL 2)|C`,
D for compact with_the_max_arc Subset of TOP-REAL 2;
registration
let M be symmetric triangle Reflexive MetrStruct, x, y be Point of M;
cluster dist(x,y) -> non negative;
end;
registration
let n be Element of NAT, x, y be Point of TOP-REAL n;
cluster dist(x,y) -> non negative;
end;
theorem :: JORDAN:1
for p1, p2 being Point of TOP-REAL n st p1 <> p2 holds 1/2*(p1+p2) <> p1;
theorem :: JORDAN:2
p1`2 < p2`2 implies p1`2 < (1/2*(p1+p2))`2;
theorem :: JORDAN:3
p1`2 < p2`2 implies (1/2*(p1+p2))`2 < p2`2;
theorem :: JORDAN:4
for A being vertical Subset of TOP-REAL 2 holds A /\ B is vertical;
theorem :: JORDAN:5
for A being horizontal Subset of TOP-REAL 2 holds A /\ B is horizontal;
theorem :: JORDAN:6
p in LSeg(p1,p2) & LSeg(p1,p2) is vertical implies LSeg(p,p2) is vertical;
theorem :: JORDAN:7
p in LSeg(p1,p2) & LSeg(p1,p2) is horizontal implies LSeg(p,p2) is horizontal
;
registration
:: LSeg(NW-corner C,NE-corner C) is horizontal; ::SPRECT_3:29
let P be Subset of TOP-REAL 2;
cluster LSeg(SW-corner P,SE-corner P) -> horizontal;
cluster LSeg(NW-corner P,SW-corner P) -> vertical;
cluster LSeg(NE-corner P,SE-corner P) -> vertical;
end;
registration
let P be Subset of TOP-REAL 2;
cluster LSeg(SE-corner P,SW-corner P) -> horizontal;
cluster LSeg(SW-corner P,NW-corner P) -> vertical;
cluster LSeg(SE-corner P,NE-corner P) -> vertical;
end;
registration
cluster vertical non empty compact -> with_the_max_arc for
Subset of TOP-REAL 2;
end;
theorem :: JORDAN:8
p1`1 <= r & r <= p2`1 implies LSeg(p1,p2) meets Vertical_Line(r);
theorem :: JORDAN:9
p1`2 <= r & r <= p2`2 implies LSeg(p1,p2) meets Horizontal_Line(r);
registration
let n;
cluster empty -> bounded for Subset of TOP-REAL n;
cluster non bounded -> non empty for Subset of TOP-REAL n;
end;
registration
let n be non zero Nat;
cluster open closed non bounded convex for Subset of TOP-REAL n;
end;
theorem :: JORDAN:10
for C being compact Subset of TOP-REAL 2 holds
north_halfline UMP C \ {UMP C} misses C;
theorem :: JORDAN:11
for C being compact Subset of TOP-REAL 2 holds
south_halfline LMP C \ {LMP C} misses C;
theorem :: JORDAN:12
for C being compact Subset of TOP-REAL 2 holds
north_halfline UMP C \ {UMP C} c= UBD C;
theorem :: JORDAN:13
for C being compact Subset of TOP-REAL 2 holds
south_halfline LMP C \ {LMP C} c= UBD C;
theorem :: JORDAN:14
A is_inside_component_of B implies UBD B misses A;
theorem :: JORDAN:15
A is_outside_component_of B implies BDD B misses A;
theorem :: JORDAN:16
for n being Nat
for r being positive Real
for a being Point of TOP-REAL n holds a in Ball(a,r);
theorem :: JORDAN:17
for r being non negative Real
for p being Point of TOP-REAL n holds p is Point of Tdisk(p,r);
registration
let r be positive Real;
let n be non zero Element of NAT;
let p, q be Point of TOP-REAL n;
cluster cl_Ball(p,r) \ {q} -> non empty;
end;
theorem :: JORDAN:18
r <= s implies Ball(x,r) c= Ball(x,s);
theorem :: JORDAN:19
cl_Ball(x,r) \ Ball(x,r) = Sphere(x,r);
theorem :: JORDAN:20
y in Sphere(x,r) implies LSeg(x,y) \ {x,y} c= Ball(x,r);
theorem :: JORDAN:21
r < s implies cl_Ball(x,r) c= Ball(x,s);
theorem :: JORDAN:22
r < s implies Sphere(x,r) c= Ball(x,s);
theorem :: JORDAN:23
for r being non zero Real holds Cl Ball(x,r) = cl_Ball(x,r);
theorem :: JORDAN:24
for r being non zero Real holds Fr Ball(x,r) = Sphere(x,r);
registration
let n be non zero Element of NAT;
cluster bounded -> proper for Subset of TOP-REAL n;
end;
registration
let n;
cluster non empty closed convex bounded for Subset of TOP-REAL n;
cluster non empty open convex bounded for Subset of TOP-REAL n;
end;
registration
let n be Element of NAT;
let A be bounded Subset of TOP-REAL n;
cluster Cl A -> bounded;
end;
registration
let n be Element of NAT;
let A be bounded Subset of TOP-REAL n;
cluster Fr A -> bounded;
end;
theorem :: JORDAN:25
for A being closed Subset of TOP-REAL n, p being Point of TOP-REAL n st
not p in A ex r being positive Real st Ball(p,r) misses A;
theorem :: JORDAN:26
for A being bounded Subset of TOP-REAL n, a being Point of TOP-REAL n
ex r being positive Real st A c= Ball(a,r);
theorem :: JORDAN:27
for S, T being TopStruct, f being Function
of S, T st f is being_homeomorphism holds f is onto;
registration
let T be non empty T_2 TopSpace;
cluster -> T_2 for non empty SubSpace of T;
end;
registration
let p, r;
cluster Tdisk(p,r) -> closed;
end;
registration
let p, r;
cluster Tdisk(p,r) -> compact;
end;
begin :: Paths
theorem :: JORDAN:28
for T being non empty TopSpace, a, b being Point of T
for f being Path of a,b st a,b are_connected holds rng f is connected;
theorem :: JORDAN:29
for X being non empty TopSpace, Y being non empty SubSpace of X,
x1, x2 being Point of X, y1, y2 being Point of Y,
f being Path of x1,x2 st x1 = y1 & x2 = y2 & x1,x2 are_connected &
rng f c= the carrier of Y holds y1,y2 are_connected & f is Path of y1,y2;
theorem :: JORDAN:30
for X being pathwise_connected non empty TopSpace,
Y being non empty SubSpace of X,
x1, x2 being Point of X, y1, y2 being Point of Y,
f being Path of x1,x2 st x1 = y1 & x2 = y2 & rng f c= the carrier of Y holds
y1,y2 are_connected & f is Path of y1,y2;
theorem :: JORDAN:31
for T being non empty TopSpace, a, b being Point of T
for f being Path of a,b st a,b are_connected holds rng f = rng -f;
theorem :: JORDAN:32
for T being pathwise_connected non empty TopSpace, a, b being Point of T
for f being Path of a,b holds rng f = rng -f;
theorem :: JORDAN:33
for T being non empty TopSpace, a, b, c being Point of T
for f being Path of a,b, g being Path of b,c st
a,b are_connected & b,c are_connected holds rng f c= rng(f+g);
theorem :: JORDAN:34
for T being pathwise_connected non empty TopSpace, a, b, c being Point of T
for f being Path of a,b, g being Path of b,c holds rng f c= rng(f+g);
theorem :: JORDAN:35
for T being non empty TopSpace, a, b, c being Point of T
for f being Path of b,c, g being Path of a,b st
a,b are_connected & b,c are_connected holds rng f c= rng(g+f);
theorem :: JORDAN:36
for T being pathwise_connected non empty TopSpace, a, b, c being Point of T
for f being Path of b,c, g being Path of a,b holds rng f c= rng(g+f);
theorem :: JORDAN:37
for T being non empty TopSpace, a, b, c being Point of T
for f being Path of a,b, g being Path of b,c st
a,b are_connected & b,c are_connected holds rng(f+g) = rng f \/ rng g;
theorem :: JORDAN:38
for T being pathwise_connected non empty TopSpace, a, b, c being Point of T
for f being Path of a,b, g being Path of b,c holds rng(f+g) = rng f \/ rng g;
theorem :: JORDAN:39
for T being non empty TopSpace, a, b, c, d being Point of T
for f being Path of a,b, g being Path of b,c, h being Path of c,d st
a,b are_connected & b,c are_connected & c,d are_connected holds
rng(f+g+h) = rng f \/ rng g \/ rng h;
theorem :: JORDAN:40
for T being pathwise_connected non empty TopSpace,
a, b, c, d being Point of T
for f being Path of a,b, g being Path of b,c, h being Path of c,d
holds rng(f+g+h) = rng f \/ rng g \/ rng h;
theorem :: JORDAN:41
for T being non empty TopSpace, a being Point of T holds
I[01] --> a is Path of a,a;
theorem :: JORDAN:42
for p1, p2 being Point of TOP-REAL n, P being Subset of TOP-REAL n
holds P is_an_arc_of p1,p2 implies
ex F being Path of p1,p2, f being Function of I[01], (TOP-REAL n)|P st
rng f = P & F = f;
theorem :: JORDAN:43
for p1, p2 being Point of TOP-REAL n
ex F being Path of p1,p2, f being Function
of I[01], (TOP-REAL n)|LSeg(p1,p2) st rng f = LSeg(p1,p2) & F = f;
theorem :: JORDAN:44
for p1,p2,q1,q2 being Point of TOP-REAL 2
st P is_an_arc_of p1,p2 & q1 in P & q2 in P &
q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2
ex f being Path of q1,q2 st rng f c= P & rng f misses {p1,p2};
begin :: Rectangles
theorem :: JORDAN:45
a <= b & c <= d implies
rectangle(a,b,c,d) c= closed_inside_of_rectangle(a,b,c,d);
theorem :: JORDAN:46
inside_of_rectangle(a,b,c,d) c= closed_inside_of_rectangle(a,b,c,d);
theorem :: JORDAN:47
closed_inside_of_rectangle(a,b,c,d) = outside_of_rectangle(a,b,c,d)`;
registration
let a, b, c, d be Real;
cluster closed_inside_of_rectangle(a,b,c,d) -> closed;
end;
theorem :: JORDAN:48
closed_inside_of_rectangle(a,b,c,d) misses outside_of_rectangle(a,b,c,d);
theorem :: JORDAN:49
closed_inside_of_rectangle(a,b,c,d) /\ inside_of_rectangle(a,b,c,d)
= inside_of_rectangle(a,b,c,d);
theorem :: JORDAN:50
a < b & c < d implies
Int closed_inside_of_rectangle(a,b,c,d) = inside_of_rectangle(a,b,c,d);
theorem :: JORDAN:51
a <= b & c <= d implies
closed_inside_of_rectangle(a,b,c,d) \ inside_of_rectangle(a,b,c,d)
= rectangle(a,b,c,d);
theorem :: JORDAN:52
a < b & c < d implies
Fr closed_inside_of_rectangle(a,b,c,d) = rectangle(a,b,c,d);
theorem :: JORDAN:53
a <= b & c <= d implies W-bound closed_inside_of_rectangle(a,b,c,d) = a;
theorem :: JORDAN:54
a <= b & c <= d implies S-bound closed_inside_of_rectangle(a,b,c,d) = c;
theorem :: JORDAN:55
a <= b & c <= d implies E-bound closed_inside_of_rectangle(a,b,c,d) = b;
theorem :: JORDAN:56
a <= b & c <= d implies N-bound closed_inside_of_rectangle(a,b,c,d) = d;
theorem :: JORDAN:57
a < b & c < d & p1 in closed_inside_of_rectangle(a,b,c,d) &
not p2 in closed_inside_of_rectangle(a,b,c,d) & P is_an_arc_of p1,p2 implies
Segment(P,p1,p2,p1,First_Point(P,p1,p2,rectangle(a,b,c,d))) c=
closed_inside_of_rectangle(a,b,c,d);
begin :: Some useful functions
definition
let S, T be non empty TopSpace, x be Point of [:S,T:];
redefine func x`1 -> Element of S;
redefine func x`2 -> Element of T;
end;
definition
let o be Point of TOP-REAL 2;
func diffX2_1(o) -> RealMap of [:TOP-REAL 2,TOP-REAL 2:] means
:: JORDAN:def 1
for x being Point of [:TOP-REAL 2,TOP-REAL 2:] holds it.x = x`2`1 - o`1;
func diffX2_2(o) -> RealMap of [:TOP-REAL 2,TOP-REAL 2:] means
:: JORDAN:def 2
for x being Point of [:TOP-REAL 2,TOP-REAL 2:] holds it.x = x`2`2 - o`2;
end;
definition
func diffX1_X2_1 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means
:: JORDAN:def 3
for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`1`1 - x`2`1;
func diffX1_X2_2 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means
:: JORDAN:def 4
for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`1`2 - x`2`2;
func Proj2_1 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means
:: JORDAN:def 5
for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`2`1;
func Proj2_2 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means
:: JORDAN:def 6
for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`2`2;
end;
theorem :: JORDAN:58
for o being Point of TOP-REAL 2 holds
diffX2_1(o) is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1;
theorem :: JORDAN:59
for o being Point of TOP-REAL 2 holds
diffX2_2(o) is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1;
theorem :: JORDAN:60
diffX1_X2_1 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1;
theorem :: JORDAN:61
diffX1_X2_2 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1;
theorem :: JORDAN:62
Proj2_1 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1;
theorem :: JORDAN:63
Proj2_2 is continuous Function of [:TOP-REAL 2, TOP-REAL 2:], R^1;
registration
let o be Point of TOP-REAL 2;
cluster diffX2_1(o) -> continuous;
cluster diffX2_2(o) -> continuous;
end;
registration
cluster diffX1_X2_1 -> continuous;
cluster diffX1_X2_2 -> continuous;
cluster Proj2_1 -> continuous;
cluster Proj2_2 -> continuous;
end;
definition
let n be non zero Element of NAT, o, p be Point of TOP-REAL n,
r be positive Real such that
p is Point of Tdisk(o,r);
func DiskProj(o,r,p) -> Function
of (TOP-REAL n)|(cl_Ball(o,r)\{p}), Tcircle(o,r) means
:: JORDAN:def 7
for x being Point of (TOP-REAL n)|(cl_Ball(o,r)\{p})
ex y being Point of TOP-REAL n st x = y & it.x = HC(p,y,o,r);
end;
theorem :: JORDAN:64
for o, p being Point of TOP-REAL 2,
r being positive Real st p is Point of Tdisk(o,r) holds
DiskProj(o,r,p) is continuous;
theorem :: JORDAN:65
for n being non zero Element of NAT, o, p being Point of TOP-REAL n,
r being positive Real st p in Ball(o,r) holds
DiskProj(o,r,p)|Sphere(o,r) = id Sphere(o,r);
definition
let n be non zero Element of NAT, o, p be Point of TOP-REAL n,
r be positive Real such that
p in Ball(o,r);
func RotateCircle(o,r,p) -> Function of Tcircle(o,r), Tcircle(o,r) means
:: JORDAN:def 8
for x being Point of Tcircle(o,r)
ex y being Point of TOP-REAL n st x = y & it.x = HC(y,p,o,r);
end;
theorem :: JORDAN:66
for o, p being Point of TOP-REAL 2,
r being positive Real st p in Ball(o,r) holds
RotateCircle(o,r,p) is continuous;
theorem :: JORDAN:67
for n being non zero Element of NAT for o, p being Point of TOP-REAL n,
r being positive Real st p in Ball(o,r)
holds RotateCircle(o,r,p) is without_fixpoints;
begin :: Jordan's Curve Theorem
theorem :: JORDAN:68
U = P & U is a_component &
V is a_component & U <> V implies Cl P misses V;
theorem :: JORDAN:69
U is a_component implies
(TOP-REAL 2)|C`|U is pathwise_connected;
theorem :: JORDAN:70
for h being Homeomorphism of TOP-REAL 2 holds
h.:C is being_simple_closed_curve;
theorem :: JORDAN:71
|[-1,0]|,|[1,0]| realize-max-dist-in P implies
P c= closed_inside_of_rectangle(-1,1,-3,3);
theorem :: JORDAN:72
|[-1,0]|,|[1,0]| realize-max-dist-in P implies
P misses LSeg(|[-1,3]|,|[1,3]|);
theorem :: JORDAN:73
|[-1,0]|,|[1,0]| realize-max-dist-in P implies
P misses LSeg(|[-1,-3]|,|[1,-3]|);
theorem :: JORDAN:74
|[-1,0]|,|[1,0]| realize-max-dist-in P implies
P /\ rectangle(-1,1,-3,3) = {|[-1,0]|,|[1,0]|};
theorem :: JORDAN:75
|[-1,0]|,|[1,0]| realize-max-dist-in P implies W-bound P = -1;
theorem :: JORDAN:76
|[-1,0]|,|[1,0]| realize-max-dist-in P implies E-bound P = 1;
theorem :: JORDAN:77
for P being compact Subset of TOP-REAL 2 holds
|[-1,0]|,|[1,0]| realize-max-dist-in P implies W-most P = {|[-1,0]|};
theorem :: JORDAN:78
for P being compact Subset of TOP-REAL 2 holds
|[-1,0]|,|[1,0]| realize-max-dist-in P implies E-most P = {|[1,0]|};
theorem :: JORDAN:79
for P being compact Subset of TOP-REAL 2 holds
|[-1,0]|,|[1,0]| realize-max-dist-in P implies
W-min P = |[-1,0]| & W-max P = |[-1,0]|;
theorem :: JORDAN:80
for P being compact Subset of TOP-REAL 2 holds
|[-1,0]|,|[1,0]| realize-max-dist-in P implies
E-min P = |[1,0]| & E-max P = |[1,0]|;
theorem :: JORDAN:81
|[-1,0]|,|[1,0]| realize-max-dist-in P implies
LSeg(|[0,3]|,UMP P) is vertical;
theorem :: JORDAN:82
|[-1,0]|,|[1,0]| realize-max-dist-in P implies
LSeg(LMP P,|[0,-3]|) is vertical;
theorem :: JORDAN:83
|[-1,0]|,|[1,0]| realize-max-dist-in P & p in P implies p`2 < 3;
theorem :: JORDAN:84
|[-1,0]|,|[1,0]| realize-max-dist-in P & p in P implies -3 < p`2;
theorem :: JORDAN:85
|[-1,0]|,|[1,0]| realize-max-dist-in D & p in LSeg(|[0,3]|,UMP D) implies
(UMP D)`2 <= p`2;
theorem :: JORDAN:86
|[-1,0]|,|[1,0]| realize-max-dist-in D & p in LSeg(LMP D,|[0,-3]|) implies
p`2 <= (LMP D)`2;
theorem :: JORDAN:87
|[-1,0]|,|[1,0]| realize-max-dist-in D implies
LSeg(|[0,3]|,UMP D) c= north_halfline UMP D;
theorem :: JORDAN:88
|[-1,0]|,|[1,0]| realize-max-dist-in D implies
LSeg(LMP D,|[0,-3]|) c= south_halfline LMP D;
theorem :: JORDAN:89
|[-1,0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies
LSeg(|[0,3]|,UMP C) misses P;
theorem :: JORDAN:90
|[-1,0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies
LSeg(LMP C,|[0,-3]|) misses P;
theorem :: JORDAN:91
|[-1,0]|,|[1,0]| realize-max-dist-in D implies
LSeg(|[0,3]|,UMP D) /\ D = {UMP D};
theorem :: JORDAN:92
|[-1,0]|,|[1,0]| realize-max-dist-in D implies
LSeg(|[0,-3]|,LMP D) /\ D = {LMP D};
theorem :: JORDAN:93
P is compact &
|[-1,0]|,|[1,0]| realize-max-dist-in P & A is_inside_component_of P implies
A c= closed_inside_of_rectangle(-1,1,-3,3);
theorem :: JORDAN:94
|[-1,0]|,|[1,0]| realize-max-dist-in C implies LSeg(|[0,3]|,|[0,-3]|) meets C
;
theorem :: JORDAN:95
|[-1,0]|,|[1,0]| realize-max-dist-in C implies
for Jc, Jd being compact with_the_max_arc Subset of TOP-REAL 2 st
Jc is_an_arc_of |[-1,0]|,|[1,0]| & Jd is_an_arc_of |[-1,0]|,|[1,0]| &
C = Jc \/ Jd & Jc /\ Jd = {|[-1,0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd &
W-bound C = W-bound Jc & E-bound C = E-bound Jc
for Ux being Subset of TOP-REAL 2 st Ux = Component_of Down ((1/2) *
((UMP (LSeg(LMP Jc,|[0,-3]|) /\ Jd)) + LMP Jc), C`)
holds Ux is_inside_component_of C & for V being Subset of TOP-REAL 2 st
V is_inside_component_of C holds V = Ux;
theorem :: JORDAN:96
|[-1,0]|,|[1,0]| realize-max-dist-in C implies
for Jc, Jd being compact with_the_max_arc Subset of TOP-REAL 2 st
Jc is_an_arc_of |[-1,0]|,|[1,0]| & Jd is_an_arc_of |[-1,0]|,|[1,0]| &
C = Jc \/ Jd & Jc /\ Jd = {|[-1,0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd &
W-bound C = W-bound Jc & E-bound C = E-bound Jc holds
BDD C = Component_of Down ((1/2) *
((UMP (LSeg(LMP Jc,|[0,-3]|) /\ Jd)) + LMP Jc), C`);
registration :: do not remove it
let C;
cluster BDD C -> non empty;
end;
theorem :: JORDAN:97
U = P & U is a_component implies C = Fr P;
theorem :: JORDAN:98 :: Jordan's Curve Theorem
for C being Simple_closed_curve ex A1, A2 being Subset of TOP-REAL 2 st
C` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 &
for C1, C2 being Subset of (TOP-REAL 2)|C` st C1 = A1 & C2 = A2 holds
C1 is a_component & C2 is a_component;
::$N Jordan Curve Theorem
theorem :: JORDAN:99
for C being Simple_closed_curve holds C is Jordan;