:: The Jordan's Property for Certain Subsets of the Plane
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992-2026 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, XBOOLE_0, PRE_TOPC, REAL_1, CARD_1, XXREAL_1, XXREAL_0,
FUNCT_1, BORSUK_1, ORDINAL2, RELAT_2, RELAT_1, SUBSET_1, FUNCOP_1,
CONNSP_1, EUCLID, RLVECT_1, CONVEX1, RLTOPSP1, TARSKI, TOPREAL1, TOPS_2,
STRUCT_0, ARYTM_3, MCART_1, ARYTM_1, PCOMPS_1, RCOMP_1, METRIC_1,
SQUARE_1, JORDAN1, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, XREAL_0,
REAL_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, NUMBERS, PRE_TOPC, TOPS_2,
CONNSP_1, SQUARE_1, RCOMP_1, STRUCT_0, METRIC_1, PCOMPS_1, BORSUK_1,
TOPREAL1, RLVECT_1, RLTOPSP1, EUCLID;
constructors REAL_1, SQUARE_1, RCOMP_1, CONNSP_1, TOPS_2, TOPMETR, TOPREAL1,
FUNCOP_1, FUNCSDOM, CONVEX1, BINOP_2, PCOMPS_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, MEMBERED, STRUCT_0,
PRE_TOPC, BORSUK_1, EUCLID, RLTOPSP1, SQUARE_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, CONNSP_1, XBOOLE_0;
equalities EUCLID, SQUARE_1, SUBSET_1, STRUCT_0, PCOMPS_1, RLTOPSP1;
expansions TARSKI, CONNSP_1, XBOOLE_0;
theorems TARSKI, FUNCOP_1, FUNCT_1, FUNCT_2, SUBSET_1, RCOMP_1, METRIC_1,
PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, CONNSP_1, SQUARE_1, TOPMETR,
TOPREAL1, EUCLID, TOPREAL3, TREAL_1, XBOOLE_0, XBOOLE_1, XREAL_1,
ZFMISC_1, SPPOL_1, XXREAL_0, RLTOPSP1;
begin
::
:: Selected theorems on connected space
::
reserve GX,GY for non empty TopSpace,
x,y for Point of GX,
r,s for Real;
Lm1: 0 in [.0,1.] & 1 in [.0,1.]
proof
A1: 0 in {r:0<=r & r<=1};
1 in {s:0<=s & s<=1};
hence thesis by A1,RCOMP_1:def 1;
end;
theorem Th1: ::Arcwise connectedness derives connectedness
for GX being non empty TopSpace st (for x,y being Point of GX
ex h being Function of I[01],GX st h is continuous & x=h.0 & y=h.1)
holds GX is connected
proof
let GX;
assume
A1: for x,y being Point of GX
ex h being Function of I[01],GX st h is continuous & x=h.0 & y=h.1;
for x,y being Point of GX ex GY st (GY is connected &
ex f being Function of GY,GX st f is continuous & x in rng(f)& y in rng(f))
proof
let x,y;
now
consider h being Function of I[01],GX such that
A2: h is continuous and
A3: x=h.0 and
A4: y=h.1 by A1;
A5: 0 in dom h by Lm1,BORSUK_1:40,FUNCT_2:def 1;
A6: 1 in dom h by Lm1,BORSUK_1:40,FUNCT_2:def 1;
A7: x in rng h by A3,A5,FUNCT_1:def 3;
y in rng h by A4,A6,FUNCT_1:def 3;
hence thesis by A2,A7,TREAL_1:19;
end;
hence thesis;
end;
hence thesis by TOPS_2:63;
end;
theorem Th2: ::Arcwise connectedness derives connectedness for subset
for A being Subset of GX st
(for xa,ya being Point of GX st xa in A & ya in A & xa<>ya
ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1)
holds A is connected
proof
let A be Subset of GX;
assume that
A1: for xa,ya being Point of GX st xa in A & ya in A & xa<>ya
ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1;
per cases;
suppose A is non empty;
then reconsider A as non empty Subset of GX;
A2: for xa,ya being Point of GX st xa in A & ya in A & xa = ya
ex h being Function of I[01],GX|A st h is continuous & xa=h.0 & ya=h.1
proof
let xa,ya be Point of GX;
assume that
A3: xa in A and ya in A and
A4: xa = ya;
reconsider xa9 = xa as Element of GX|A by A3,PRE_TOPC:8;
reconsider h = I[01] --> xa9 as Function of I[01], GX|A;
take h;
thus thesis by A4,Lm1,BORSUK_1:40,FUNCOP_1:7;
end;
for xb,yb being Point of GX|A
ex ha being Function of I[01],GX|A st ha is continuous & xb=ha.0 & yb=ha.1
proof
let xb,yb be Point of GX|A;
A5: xb in [#](GX|A);
A6: yb in [#](GX|A);
A7: xb in A by A5,PRE_TOPC:def 5;
A8: yb in A by A6,PRE_TOPC:def 5;
per cases;
suppose xb<>yb;
hence thesis by A1,A7,A8;
end;
suppose xb = yb;
hence thesis by A2,A7;
end;
end;
then GX|A is connected by Th1;
hence thesis;
end;
suppose A is empty;
then reconsider D = A as empty Subset of GX;
let A1, B1 be Subset of GX|A such that
[#](GX|A) = A1 \/ B1 and A1,B1 are_separated;
[#](GX|D) = D;
hence thesis;
end;
end;
theorem
for A0 being Subset of GX, A1 being Subset of GX st
A0 is connected & A1 is connected & A0 meets A1
holds A0 \/ A1 is connected by CONNSP_1:1,17;
theorem Th4:
for A0,A1,A2 being Subset of GX st
A0 is connected & A1 is connected & A2 is connected & A0 meets A1 &
A1 meets A2 holds A0 \/ A1 \/ A2 is connected
proof
let A0,A1,A2 be Subset of GX;
assume that
A1: A0 is connected and
A2: A1 is connected and
A3: A2 is connected and
A4: A0 meets A1 and
A5: A1 meets A2;
A6: A1 /\ A2 <> {} by A5;
A7: A0 \/ A1 is connected by A1,A2,A4,CONNSP_1:1,17;
(A0 \/ A1)/\ A2= A0 /\ A2 \/ A1 /\ A2 by XBOOLE_1:23;
then (A0 \/ A1) meets A2 by A6;
hence thesis by A3,A7,CONNSP_1:1,17;
end;
theorem Th5:
for A0,A1,A2,A3 being Subset of GX st A0 is connected & A1 is connected &
A2 is connected & A3 is connected & A0 meets A1 & A1 meets A2 &
A2 meets A3 holds A0 \/ A1 \/ A2 \/ A3 is connected
proof
let A0,A1,A2,A3 be Subset of GX;
assume that
A1: A0 is connected and
A2: A1 is connected and
A3: A2 is connected and
A4: A3 is connected and
A5: A0 meets A1 and
A6: A1 meets A2 and
A7: A2 meets A3;
A8: A2 /\ A3 <> {} by A7;
A9: A0 \/ A1 \/ A2 is connected by A1,A2,A3,A5,A6,Th4;
(A0 \/ A1 \/ A2)/\ A3= (A0 \/ A1) /\ A3 \/ A2 /\ A3 by XBOOLE_1:23;
then (A0 \/ A1 \/ A2) meets A3 by A8;
hence thesis by A4,A9,CONNSP_1:1,17;
end;
begin
::
:: Certain connected and open subsets in the Euclidean plane
::
reserve Q,P1,P2 for Subset of TOP-REAL 2;
reserve P for Subset of TOP-REAL 2;
reserve w1,w2 for Point of TOP-REAL 2;
definition
let V be RealLinearSpace, P be Subset of V;
redefine attr P is convex means :: redefines convex (RLTOPSP1, redefinition) → convex (CONVEX1, definition)
for w1,w2 being Element of V st w1 in P & w2 in P holds LSeg(w1,w2) c= P;
compatibility by RLTOPSP1:22;
end;
registration let n be Nat;
cluster convex -> connected for Subset of TOP-REAL n;
coherence
proof
let P be Subset of TOP-REAL n;
assume that
A1: for w3,w4 being Point of TOP-REAL n st w3 in P & w4 in P holds
LSeg(w3,w4) c= P;
for w1,w2 being Point of TOP-REAL n st w1 in P & w2 in P & w1<>w2
ex h being Function of I[01],(TOP-REAL n)|P st h is continuous
& w1=h.0 & w2=h.1
proof
let w1,w2 be Point of TOP-REAL n;
assume that
A2: w1 in P and
A3: w2 in P and
A4: w1<>w2;
A5: LSeg(w1,w2) c= P by A1,A2,A3;
LSeg(w1,w2) is_an_arc_of w1,w2 by A4,TOPREAL1:9;
then consider f being Function of I[01], (TOP-REAL n)|LSeg(w1,w2) such that
A6: f is being_homeomorphism and
A7: f.0 = w1 and
A8: f.1 = w2 by TOPREAL1:def 1;
A9: f is continuous by A6,TOPS_2:def 5;
A10: rng f = [#]((TOP-REAL n)|LSeg(w1,w2)) by A6,TOPS_2:def 5;
then
A11: rng f c= P by A5,PRE_TOPC:def 5;
then [#]((TOP-REAL n)|LSeg(w1,w2)) c= [#]((TOP-REAL n)|P)
by A10,PRE_TOPC:def 5;
then
A12: (TOP-REAL n)|LSeg(w1,w2) is SubSpace of (TOP-REAL n)|P by TOPMETR:3;
dom f=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then reconsider g=f as Function of [.0,1.],P by A11,FUNCT_2:2;
the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P)
.= P by PRE_TOPC:def 5;
then reconsider gt=g as Function of I[01],(TOP-REAL n)|P by BORSUK_1:40;
gt is continuous by A9,A12,PRE_TOPC:26;
hence thesis by A7,A8;
end;
hence thesis by Th2;
end;
end;
reserve pa,pb for Point of TOP-REAL 2,
s1,t1,s2,t2,s,t,s3,t3,s4,t4,s5,t5,s6,t6, l,sa,sd,ta,td for Real;
reserve s1a,t1a,s2a,t2a,s3a,t3a,sb,tb,sc,tc for Real;
Lm2: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
Lm3: for s1 holds { |[ sb,tb ]|:sb<s1} is Subset of REAL 2
proof
let s1;
{ |[ sb,tb ]|:sb<s1} c= REAL 2
proof
let y be object;
assume y in { |[ sb,tb ]|:sb<s1};
then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and s7<s1;
|[ s7,t7 ]| in the carrier of TOP-REAL 2;
hence thesis by A1,EUCLID:22;
end;
hence thesis;
end;
Lm4: for t1 holds { |[ sb,tb ]| :tb<t1} is Subset of REAL 2
proof
let t1;
{ |[ sd,td ]|:td<t1} c= REAL 2
proof
let y be object;
assume y in { |[ sd,td ]|:td<t1};
then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and t7<t1;
|[ s7,t7 ]| in the carrier of TOP-REAL 2;
hence thesis by A1,EUCLID:22;
end;
hence thesis;
end;
Lm5: for s2 holds { |[ sb,tb ]| :s2<sb} is Subset of REAL 2
proof
let s2;
{ |[ sb,tb ]|:s2<sb} c= REAL 2
proof
let y be object;
assume y in { |[ sb,tb ]|:s2<sb};
then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and s2<s7;
|[ s7,t7 ]| in the carrier of TOP-REAL 2;
hence thesis by A1,EUCLID:22;
end;
hence thesis;
end;
Lm6: for t2 holds { |[ sb,tb ]|:t2<tb} is Subset of REAL 2
proof
let t2;
{ |[ sb,tb ]|:t2<tb} c= REAL 2
proof
let y be object;
assume y in { |[ sb,tb ]|:t2<tb};
then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and t2<t7;
|[ s7,t7 ]| in the carrier of TOP-REAL 2;
hence thesis by A1,EUCLID:22;
end;
hence thesis;
end;
Lm7: for s1,s2,t1,t2 holds { |[ s,t ]| where s is Real,
t is Real:
s1<s & s<s2 & t1<t & t<t2} is Subset of REAL 2
proof
let s1,s2,t1,t2;
{ |[ sb,tb ]| where sb is Real, tb is Real:
s1<sb & sb<s2 & t1<tb & tb<t2} c= REAL 2
proof
let y be object;
assume y in { |[ sb,tb ]| where sb is Real,tb is Real:
s1<sb & sb<s2 & t1<tb & tb<t2};
then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and s1<s7
and s7<s2
and t1<t7
and t7<t2;
|[ s7,t7 ]| in the carrier of TOP-REAL 2;
hence thesis by A1,EUCLID:22;
end;
hence thesis;
end;
Lm8: for s1,s2,t1,t2 holds
{ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} is Subset of REAL 2
proof
let s1,s2,t1,t2;
{ |[ sb,tb ]| where sb is Real,tb is Real:
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} c= REAL 2
proof
let y be object;
assume y in { |[ sb,tb ]| where sb is Real,tb is Real:
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
then consider s7,t7 being Real such that
A1: |[ s7,t7 ]|=y and not (s1<=s7 & s7<=s2 & t1<=t7 & t7<=t2);
|[ s7,t7 ]| in the carrier of TOP-REAL 2;
hence thesis by A1,EUCLID:22;
end;
hence thesis;
end;
::$CT
theorem Th6:
{|[ s,t ]|: s1<s & s<s2 & t1<t & t<t2} =
{|[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2} /\ {|[s5,t5]|:t1<t5} /\
{|[s6,t6]|:t6<t2}
proof
now
let x be object;
assume x in { |[ s,t ]|: s1<s & s<s2 & t1<t & t<t2};
then
A1: ex s,t st |[s,t]|=x & s1<s & s<s2 & t1<t & t<t2;
then
A2: x in { |[ s3,t3 ]|:s1<s3};
x in { |[ s4,t4 ]|:s4<s2} by A1;
then
A3: x in { |[ s3,t3 ]|:s1<s3} /\ { |[ s4,t4 ]|:s4<s2} by A2,XBOOLE_0:def 4;
A4: x in { |[ s5,t5 ]|:t1<t5} by A1;
A5: x in { |[ s6,t6 ]|:t6<t2} by A1;
x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5} by A3,A4
,XBOOLE_0:def 4;
hence
x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
/\ {|[s6,t6]|:t6<t2} by A5,XBOOLE_0:def 4;
end;
then
A6: { |[ s,t ]|: s1<s & s<s2 & t1<t & t<t2} c=
{ |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
/\ {|[s6,t6]|:t6<t2};
now
let x be object;
assume
A7: x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5 }
/\ {|[s6,t6]|:t6<t2};
then
A8: x in { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5} by
XBOOLE_0:def 4;
then
A9: x in { |[ s3,t3 ]|:s1<s3} /\ { |[ s4,t4]|:s4<s2} by XBOOLE_0:def 4;
A10: x in { |[ s6,t6 ]|:t6<t2} by A7,XBOOLE_0:def 4;
A11: x in { |[ s3,t3 ]|:s1<s3} by A9,XBOOLE_0:def 4;
A12: x in { |[ s4,t4 ]|:s4<s2} by A9,XBOOLE_0:def 4;
A13: x in { |[ s5,t5 ]|:t1<t5} by A8,XBOOLE_0:def 4;
A14: ex sa,ta st |[sa,ta]|=x & s1<sa by A11;
A15: ex sb,tb st |[sb,tb]|=x & sb< s2 by A12;
A16: ex sc,tc st |[sc,tc]|=x & t1<tc by A13;
A17: ex sd,td st |[sd,td]|=x & td<t2 by A10;
consider sa,ta such that
A18: |[sa,ta]|=x and
A19: s1<sa by A11;
reconsider p=x as Point of TOP-REAL 2 by A14;
A20: p`1=sa by A18,EUCLID:52;
A21: p`2=ta by A18,EUCLID:52;
A22: sa<s2 by A15,A20,EUCLID:52;
A23: t1<ta by A16,A21,EUCLID:52;
ta<t2 by A17,A21,EUCLID:52;
hence x in { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2} by A18,A19,A22,A23;
end;
then { |[ s3,t3 ]|:s1<s3} /\ {|[s4,t4]|:s4<s2}/\ {|[s5,t5]|:t1<t5}
/\ {|[s6,t6]|:t6<t2}c={ |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
hence thesis by A6;
end;
theorem Th7:
{|[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} =
{|[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1} \/ {|[s5,t5]|:s2<s5} \/
{|[s6,t6]|:t2<t6}
proof
now
let x be object;
assume x in { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
then ex s,t st |[s,t]|=x & not (s1<=s & s<=s2 & t1<=t & t<=t2);
then x in { |[ s3,t3 ]|:s3<s1}or x in { |[ s4,t4 ]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6};
then x in { |[ s3,t3 ]|:s3<s1} \/ { |[ s4,t4 ]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3;
then x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3;
hence
x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6} by XBOOLE_0:def 3;
end;
then
A1: { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} c=
{ |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6};
now
let x be object;
assume x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2< s5
} \/ {|[s6,t6]|:t2<t6};
then x in { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3;
then x in { |[ s3,t3 ]|:s3<s1} \/ { |[ s4,t4]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3
;
then x in { |[ s3,t3 ]|:s3<s1} or x in { |[ s4,t4 ]|:t4<t1}
or x in { |[ s5,t5 ]|:s2<s5} or x in { |[ s6,t6 ]|:t2<t6} by XBOOLE_0:def 3
;
then (ex sa,ta st |[sa,ta]|=x & sa<s1)
or (ex sc,tc st |[sc,tc]|=x & tc<t1) or (ex sb,tb st |[sb,tb]|=x & s2<sb)
or ex sd,td st |[sd,td]|=x & t2<td;
hence x in { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
end;
then { |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6}c={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
hence thesis by A1;
end;
theorem Th8:
for s1,t1,s2,t2,P st P = {|[ s,t ]|:s1<s & s<s2 & t1<t & t<t2}
holds P is convex
proof
let s1,t1,s2,t2,P;
assume
A1: P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
let x be object such that
A4: x in LSeg(w1,w2);
consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: s1<s3 and
A7: s3<s2 and
A8: t1<t3 and
A9: t3<t2 by A1,A2;
A10: w1`1=s3 by A5,EUCLID:52;
A11: w1`2=t3 by A5,EUCLID:52;
consider s4,t4 such that
A12: |[ s4,t4 ]|=w2 and
A13: s1<s4 and
A14: s4<s2 and
A15: t1<t4 and
A16: t4<t2 by A1,A3;
A17: w2`1=s4 by A12,EUCLID:52;
A18: w2`2=t4 by A12,EUCLID:52;
consider l such that
A19: x = (1-l)*w1 + l*w2 and
A20: 0 <= l and
A21: l <= 1 by A4;
set w = (1-l)*w1 + l*w2;
A22: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A23: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A24: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A25: ((1-l)*w1)`1= (1-l)*w1`1 by A23,EUCLID:52;
A26: ((1-l)*w1)`2= (1-l)*w1`2 by A23,EUCLID:52;
A27: (l*w2)`1=l*w2`1 by A24,EUCLID:52;
A28: (l*w2)`2=l*w2`2 by A24,EUCLID:52;
A29: w`1=(1-l)* w1`1+ l* w2`1 by A22,A25,A27,EUCLID:52;
A30: w`2=(1-l)* w1`2+ l* w2`2 by A22,A26,A28,EUCLID:52;
A31: s1< w`1 by A6,A10,A13,A17,A20,A21,A29,XREAL_1:175;
A32: w`1<s2 by A7,A10,A14,A17,A20,A21,A29,XREAL_1:176;
A33: t1< w`2 by A8,A11,A15,A18,A20,A21,A30,XREAL_1:175;
A34: w`2<t2 by A9,A11,A16,A18,A20,A21,A30,XREAL_1:176;
w = |[w`1, w`2]| by EUCLID:53;
hence thesis by A1,A19,A31,A32,A33,A34;
end;
::$CT
theorem Th9:
for s1,P st P = { |[ s,t ]|:s1<s } holds P is convex
proof
let s1,P;
assume
A1: P = { |[ s,t ]|:s1<s };
let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
let x be object such that
A4: x in LSeg(w1,w2);
consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: s1<s3 by A1,A2;
A7: w1`1=s3 by A5,EUCLID:52;
consider s4,t4 such that
A8: |[ s4,t4 ]|=w2 and
A9: s1<s4 by A1,A3;
A10: w2`1=s4 by A8,EUCLID:52;
consider l such that
A11: x = (1-l)*w1 + l*w2 and
A12: 0 <= l and
A13: l <= 1 by A4;
set w = (1-l)*w1 + l*w2;
A14: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A15: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A16: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A17: ((1-l)*w1)`1= (1-l)*w1`1 by A15,EUCLID:52;
(l*w2)`1=l*w2`1 by A16,EUCLID:52;
then w`1=(1-l)* w1`1+ l* w2`1 by A14,A17,EUCLID:52;
then
A18: s1< w`1 by A6,A7,A9,A10,A12,A13,XREAL_1:175;
w = |[w`1, w`2]| by EUCLID:53;
hence thesis by A1,A11,A18;
end;
::$CT
theorem Th10:
for s2,P st P = {|[ s,t ]|:s<s2 } holds P is convex
proof
let s2,P;
assume
A1: P = { |[ s,t ]|:s<s2 };
let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
let x be object such that
A4: x in LSeg(w1,w2);
consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: s3<s2 by A1,A2;
A7: w1`1=s3 by A5,EUCLID:52;
consider s4,t4 such that
A8: |[ s4,t4 ]|=w2 and
A9: s4<s2 by A1,A3;
A10: w2`1=s4 by A8,EUCLID:52;
consider l such that
A11: x = (1-l)*w1 + l*w2 and
A12: 0 <= l and
A13: l <= 1 by A4;
set w = (1-l)*w1 + l*w2;
A14: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A15: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A16: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A17: ((1-l)*w1)`1= (1-l)*w1`1 by A15,EUCLID:52;
(l*w2)`1=l*w2`1 by A16,EUCLID:52;
then w`1=(1-l)* w1`1+ l* w2`1 by A14,A17,EUCLID:52;
then
A18: s2> w`1 by A6,A7,A9,A10,A12,A13,XREAL_1:176;
w = |[w`1, w`2]| by EUCLID:53;
hence thesis by A1,A11,A18;
end;
::$CT
theorem Th11:
for t1,P st P = {|[ s,t ]|:t1<t } holds P is convex
proof
let t1,P;
assume
A1: P = { |[ s,t ]|:t1<t };
let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
let x be object such that
A4: x in LSeg(w1,w2);
consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: t1<t3 by A1,A2;
A7: w1`2=t3 by A5,EUCLID:52;
consider s4,t4 such that
A8: |[ s4,t4 ]|=w2 and
A9: t1<t4 by A1,A3;
A10: w2`2=t4 by A8,EUCLID:52;
consider l such that
A11: x = (1-l)*w1 + l*w2 and
A12: 0 <= l and
A13: l <= 1 by A4;
set w = (1-l)*w1 + l*w2;
A14: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A15: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A16: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A17: ((1-l)*w1)`2= (1-l)*w1`2 by A15,EUCLID:52;
(l*w2)`2=l*w2`2 by A16,EUCLID:52;
then w`2=(1-l)* w1`2+ l* w2`2 by A14,A17,EUCLID:52;
then
A18: t1< w`2 by A6,A7,A9,A10,A12,A13,XREAL_1:175;
w = |[w`1, w`2]| by EUCLID:53;
hence thesis by A1,A11,A18;
end;
::$CT
theorem Th12:
for t2,P st P = { |[ s,t ]|: t<t2 } holds P is convex
proof
let t2,P;
assume
A1: P = { |[ s,t ]|:t<t2 };
let w1,w2 such that
A2: w1 in P and
A3: w2 in P;
let x be object such that
A4: x in LSeg(w1,w2);
consider s3,t3 such that
A5: |[ s3,t3 ]|=w1 and
A6: t3<t2 by A1,A2;
A7: w1`2=t3 by A5,EUCLID:52;
consider s4,t4 such that
A8: |[ s4,t4 ]|=w2 and
A9: t4<t2 by A1,A3;
A10: w2`2=t4 by A8,EUCLID:52;
consider l such that
A11: x = (1-l)*w1 + l*w2 and
A12: 0 <= l and
A13: l <= 1 by A4;
set w = (1-l)*w1 + l*w2;
A14: w= |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A15: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
A16: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
A17: ((1-l)*w1)`2= (1-l)*w1`2 by A15,EUCLID:52;
(l*w2)`2=l*w2`2 by A16,EUCLID:52;
then w`2=(1-l)* w1`2+ l* w2`2 by A14,A17,EUCLID:52;
then
A18: t2> w`2 by A6,A7,A9,A10,A12,A13,XREAL_1:176;
w = |[w`1, w`2]| by EUCLID:53;
hence thesis by A1,A11,A18;
end;
::$CT
theorem Th13:
for s1,t1,s2,t2,P st P = { |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)}
holds P is connected
proof
let s1,t1,s2,t2,P;
assume P={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
then
A1: P={ |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6} by Th7;
reconsider A0={ |[ s,t ]|:s<s1}, A1={ |[ s,t ]|:t<t1},
A2={ |[ s,t ]|:s2<s}, A3={ |[ s,t ]|:t2<t}
as Subset of TOP-REAL 2 by Lm2,Lm3,Lm4,Lm5,Lm6;
A2: s1-1<s1 by XREAL_1:44;
A3: t1-1<t1 by XREAL_1:44;
A4: |[s1-1,t1-1]| in A0 by A2;
|[s1-1,t1-1]| in A1 by A3;
then A0 /\ A1 <> {} by A4,XBOOLE_0:def 4;
then
A5: A0 meets A1;
A6: s2< s2+1 by XREAL_1:29;
A7: |[s2+1,t1-1]| in A1 by A3;
|[s2+1,t1-1]| in A2 by A6;
then A1 /\ A2 <> {} by A7,XBOOLE_0:def 4;
then
A8: A1 meets A2;
A9: t2< t2+1 by XREAL_1:29;
A10: |[s2+1,t2+1]| in A2 by A6;
|[s2+1,t2+1]| in A3 by A9;
then A2 /\ A3 <> {} by A10,XBOOLE_0:def 4;
then
A11: A2 meets A3;
A12: A0 is convex by Th10;
A13: A1 is convex by Th12;
A14: A2 is convex by Th9;
A3 is convex by Th11;
hence thesis by A1,A5,A8,A11,A12,A13,A14,Th5;
end;
Lm9: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
theorem Th14:
for s1 holds { |[ s,t ]|:s1<s } is open Subset of TOP-REAL 2
proof
let s1;
reconsider P= { |[ s,t ]|:s1<s } as Subset of REAL 2 by Lm5;
reconsider PP=P as Subset of TopSpaceMetr Euclid 2;
for pe being Point of Euclid 2 st pe in P ex r being Real st r>0 &
Ball(pe,r) c= P
proof
let pe be Point of Euclid 2;
assume pe in P;
then consider s,t such that
A1: |[ s,t ]|=pe and
A2: s1<s;
set r=(s-s1)/2;
A3: s-s1>0 by A2,XREAL_1:50;
then
A4: r>0 by XREAL_1:139;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)<r} by METRIC_1:17;
then consider q being Element of Euclid 2 such that
A5: q=x and
A6: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by EUCLID:22;
(Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then
A7: sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A6,TOPREAL3:7;
A8: 0 <= (ppe`1 - pq`1)^2 by XREAL_1:63;
0 <= (ppe`2 - pq`2)^2 by XREAL_1:63;
then
A9: 0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A8,XREAL_1:7;
then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 2;
then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
by A7,SQUARE_1:16;
then
A10: (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A9,SQUARE_1:def 2;
(ppe`1 - pq`1)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by XREAL_1:31,63;
then (ppe`1 - pq`1)^2 <r^2 by A10,XXREAL_0:2;
then ppe`1 - pq`1 < r by A4,SQUARE_1:15;
then ppe`1 <pq`1+r by XREAL_1:19;
then ppe`1 - r < pq`1 by XREAL_1:19;
then
A11: s-(s-s1)/2 < pq`1 by A1,EUCLID:52;
s-(s-s1)/2 =r+s1;
then
A12: s1< s-(s-s1)/2 by A3,XREAL_1:29,139;
A13: |[pq`1,pq`2]|=x by A5,EUCLID:53;
s1<pq`1 by A11,A12,XXREAL_0:2;
hence thesis by A13;
end;
hence thesis by A3,XREAL_1:139;
end;
then PP is open by TOPMETR:15;
hence thesis by Lm9,PRE_TOPC:30;
end;
theorem Th15:
for s1 holds { |[ s,t ]|:s1>s } is open Subset of TOP-REAL 2
proof
let s1;
reconsider P= { |[ s,t ]|:s1>s } as Subset of REAL 2 by Lm3;
reconsider PP=P as Subset of TopSpaceMetr Euclid 2;
for pe being Point of Euclid 2 st pe in P ex r being Real st
r>0 & Ball(pe,r) c= P
proof
let pe be Point of Euclid 2;
assume pe in P;
then consider s,t such that
A1: |[ s,t ]|=pe and
A2: s1>s;
set r=(s1-s)/2;
A3: s1-s>0 by A2,XREAL_1:50;
then
A4: r>0 by XREAL_1:139;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)<r} by METRIC_1:17;
then consider q being Element of Euclid 2 such that
A5: q=x and
A6: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by EUCLID:22;
(Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then
A7: sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A6,TOPREAL3:7;
A8: 0 <= (ppe`1 - pq`1)^2 by XREAL_1:63;
0 <= (ppe`2 - pq`2)^2 by XREAL_1:63;
then
A9: 0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A8,XREAL_1:7;
then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 2;
then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
by A7,SQUARE_1:16;
then
A10: (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A9,SQUARE_1:def 2;
(ppe`1 - pq`1)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by XREAL_1:31,63;
then (pq`1-ppe`1)^2 <r^2 by A10,XXREAL_0:2;
then pq`1-ppe`1 < r by A4,SQUARE_1:15;
then ppe`1 + r > pq`1 by XREAL_1:19;
then
A11: s+(s1-s)/2 > pq`1 by A1,EUCLID:52;
s+(s1-s)/2 =s1-r;
then
A12: s1> s+(s1-s)/2 by A3,XREAL_1:44,139;
A13: |[pq`1,pq`2]|=x by A5,EUCLID:53;
s1>pq`1 by A11,A12,XXREAL_0:2;
hence thesis by A13;
end;
hence thesis by A3,XREAL_1:139;
end;
then PP is open by TOPMETR:15;
hence thesis by Lm9,PRE_TOPC:30;
end;
theorem Th16:
for s1 holds { |[ s,t ]|:s1<t } is open Subset of TOP-REAL 2
proof
let s1;
reconsider P= { |[ s,t ]|:s1<t } as Subset of REAL 2 by Lm6;
reconsider PP=P as Subset of TopSpaceMetr Euclid 2;
for pe being Point of Euclid 2 st pe in P ex r being Real
st r>0 & Ball(pe,r) c= P
proof
let pe be Point of Euclid 2;
assume pe in P;
then consider s,t such that
A1: |[ s,t ]|=pe and
A2: s1<t;
set r=(t-s1)/2;
A3: t-s1>0 by A2,XREAL_1:50;
then
A4: r>0 by XREAL_1:139;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)<r} by METRIC_1:17;
then consider q being Element of Euclid 2 such that
A5: q=x and
A6: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by EUCLID:22;
(Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then
A7: sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A6,TOPREAL3:7;
A8: 0 <= (ppe`1 - pq`1)^2 by XREAL_1:63;
0 <= (ppe`2 - pq`2)^2 by XREAL_1:63;
then
A9: 0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A8,XREAL_1:7;
then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 2;
then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
by A7,SQUARE_1:16;
then
A10: (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A9,SQUARE_1:def 2;
(ppe`2 - pq`2)^2 <= (ppe`2 - pq`2)^2+(ppe`1 - pq`1)^2 by XREAL_1:31,63;
then (ppe`2 - pq`2)^2 <r^2 by A10,XXREAL_0:2;
then ppe`2 - pq`2 < r by A4,SQUARE_1:15;
then ppe`2 <pq`2+r by XREAL_1:19;
then ppe`2 - r < pq`2 by XREAL_1:19;
then
A11: t-(t-s1)/2 < pq`2 by A1,EUCLID:52;
t-(t-s1)/2 =r+s1;
then
A12: s1< t-(t-s1)/2 by A3,XREAL_1:29,139;
A13: |[pq`1,pq`2]|=x by A5,EUCLID:53;
s1<pq`2 by A11,A12,XXREAL_0:2;
hence thesis by A13;
end;
hence thesis by A3,XREAL_1:139;
end;
then PP is open by TOPMETR:15;
hence thesis by Lm9,PRE_TOPC:30;
end;
theorem Th17:
for s1 holds { |[ s,t ]|:s1>t } is open Subset of TOP-REAL 2
proof
let s1;
reconsider P= { |[ s,t ]|:s1>t } as Subset of REAL 2 by Lm4;
reconsider PP=P as Subset of TopSpaceMetr Euclid 2;
for pe being Point of Euclid 2 st pe in P ex r being Real st r>0 &
Ball(pe,r) c= P
proof
let pe be Point of Euclid 2;
assume pe in P;
then consider s,t such that
A1: |[ s,t ]|=pe and
A2: s1>t;
set r=(s1-t)/2;
A3: s1-t>0 by A2,XREAL_1:50;
then
A4: r>0 by XREAL_1:139;
Ball(pe,r) c= P
proof
let x be object;
assume x in Ball(pe,r);
then x in {q where q is Element of Euclid 2:dist(pe,q)<r} by METRIC_1:17;
then consider q being Element of Euclid 2 such that
A5: q=x and
A6: dist(pe,q)<r;
reconsider ppe=pe, pq=q as Point of TOP-REAL 2 by EUCLID:22;
(Pitag_dist 2).(pe,q)=dist(pe,q) by METRIC_1:def 1;
then
A7: sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2)<r by A6,TOPREAL3:7;
A8: 0 <= (ppe`1 - pq`1)^2 by XREAL_1:63;
0 <= (ppe`2 - pq`2)^2 by XREAL_1:63;
then
A9: 0+0 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by A8,XREAL_1:7;
then 0 <=sqrt ( (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2) by SQUARE_1:def 2;
then (sqrt ((ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2))^2<r^2
by A7,SQUARE_1:16;
then
A10: (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 < r^2 by A9,SQUARE_1:def 2;
(ppe`2 - pq`2)^2 <= (ppe`1 - pq`1)^2 + (ppe`2 - pq`2)^2 by XREAL_1:31,63;
then (pq`2-ppe`2)^2 <r^2 by A10,XXREAL_0:2;
then pq`2-ppe`2 < r by A4,SQUARE_1:15;
then ppe`2 + r > pq`2 by XREAL_1:19;
then
A11: t+(s1-t)/2 > pq`2 by A1,EUCLID:52;
t+(s1-t)/2 =s1-r;
then
A12: s1> t+(s1-t)/2 by A3,XREAL_1:44,139;
A13: |[pq`1,pq`2]|=x by A5,EUCLID:53;
s1>pq`2 by A11,A12,XXREAL_0:2;
hence thesis by A13;
end;
hence thesis by A3,XREAL_1:139;
end;
then PP is open by TOPMETR:15;
hence thesis by Lm9,PRE_TOPC:30;
end;
theorem Th18:
for s1,t1,s2,t2 holds
{ |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2} is open Subset of TOP-REAL 2
proof
let s1,t1,s2,t2;
set P = { |[ s,t ]|:s1<s & s<s2 & t1<t & t<t2};
reconsider P1={|[s,t]|:s1<s} as Subset of TOP-REAL 2 by Lm2,Lm5;
reconsider P2={|[s,t]|:s<s2} as Subset of TOP-REAL 2 by Lm2,Lm3;
reconsider P3={|[s,t]|:t1<t} as Subset of TOP-REAL 2 by Lm2,Lm6;
reconsider P4={|[s,t]|:t<t2} as Subset of TOP-REAL 2 by Lm2,Lm4;
A1: P=P1 /\ P2 /\ P3 /\ P4 by Th6;
A2: P1 is open by Th14;
P2 is open by Th15;
then
A3: P1 /\ P2 is open by A2,TOPS_1:11;
A4: P3 is open by Th16;
A5: P4 is open by Th17;
P1 /\ P2 /\ P3 is open by A3,A4,TOPS_1:11;
hence thesis by A1,A5,TOPS_1:11;
end;
theorem Th19:
for s1,t1,s2,t2 holds
{ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)} is open Subset of TOP-REAL 2
proof
let s1,t1,s2,t2;
set P={ |[ s,t ]|:not (s1<=s & s<=s2 & t1<=t & t<=t2)};
A1: P={ |[ s3,t3 ]|:s3<s1} \/ {|[s4,t4]|:t4<t1}\/ {|[s5,t5]|:s2<s5}
\/ {|[s6,t6]|:t2<t6} by Th7;
reconsider A0={ |[ s,t ]|:s<s1} as Subset of TOP-REAL 2 by Lm2,Lm3;
reconsider A1={ |[ s,t ]|:t<t1} as Subset of TOP-REAL 2 by Lm2,Lm4;
reconsider A2={ |[ s,t ]|:s2<s} as Subset of TOP-REAL 2 by Lm2,Lm5;
reconsider A3={ |[ s,t ]|:t2<t} as Subset of TOP-REAL 2 by Lm2,Lm6;
A2: A0 is open by Th15;
A1 is open by Th17;
then
A3: A0 \/ A1 is open by A2,TOPS_1:10;
A2 is open by Th14;
then
A4: A0 \/ A1 \/ A2 is open by A3,TOPS_1:10;
A3 is open by Th16;
hence thesis by A1,A4,TOPS_1:10;
end;
theorem Th20:
for s1,t1,s2,t2,P,Q st P = { |[ sa,ta ]|:s1<sa & sa<s2 & t1<ta & ta<t2} &
Q = { |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} holds P misses Q
proof
let s1,t1,s2,t2,P,Q;
assume that
A1: P = { |[ sa,ta ]|:s1<sa & sa<s2 & t1<ta & ta<t2} and
A2: Q = { |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
assume not thesis;
then consider x be object such that
A3: x in P and
A4: x in Q by XBOOLE_0:3;
consider sa,ta such that
A5: |[sa,ta]|=x and
A6: s1<sa and
A7: sa<s2 and
A8: t1<ta and
A9: ta<t2 by A1,A3;
A10: ex sb,tb st ( |[sb,tb]|=x)&( not (s1<=sb & sb<=s2 & t1<=tb
& tb<=t2)) by A2,A4;
set p= |[sa,ta]|;
A11: p`1=sa by EUCLID:52;
p`2=ta by EUCLID:52;
hence contradiction by A5,A6,A7,A8,A9,A10,A11,EUCLID:52;
end;
theorem Th21:
for s1,s2,t1,t2 be Real holds
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} =
{|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2}
proof
let s1,s2,t1,t2;
now
let x be object;
A1: now
assume x in
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2};
then consider pp being Point of TOP-REAL 2 such that
A2: pp=x and
A3: s1<pp`1 and
A4: pp`1<s2 and
A5: t1<pp`2 and
A6: pp`2<t2;
|[pp`1,pp`2]|=x by A2,EUCLID:53;
hence
x in {|[s1a,t1a]|:s1<s1a & s1a<s2 & t1<t1a & t1a<t2} by A3,A4,A5,A6;
end;
now
assume x in {|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2};
then consider sa,ta being Real such that
A7: |[sa,ta]|=x and
A8: s1<sa and
A9: sa<s2 and
A10: t1<ta and
A11: ta<t2;
set pa=|[sa,ta]|;
A12: s1<pa`1 by A8,EUCLID:52;
A13: pa`1<s2 by A9,EUCLID:52;
A14: t1<pa`2 by A10,EUCLID:52;
pa`2<t2 by A11,EUCLID:52;
hence x in
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2}
by A7,A12,A13,A14;
end;
hence x in
{p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2}
iff x in {|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by A1;
end;
hence thesis by TARSKI:2;
end;
theorem Th22:
for s1,s2,t1,t2 holds {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} =
{|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)}
proof
let s1,s2,t1,t2;
now
let x be object;
A1: now
assume x in {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)};
then consider q being Point of TOP-REAL 2 such that
A2: q=x and
A3: not (s1<=q`1 & q`1<=s2 & t1<=q`2 & q`2<=t2);
|[q`1,q`2]|=x by A2,EUCLID:53;
hence
x in {|[s2a,t2a]| : not (s1<=s2a & s2a<=s2 & t1<=t2a & t2a<=t2)} by A3;
end;
now
assume x in {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)};
then consider sb,tb being Real such that
A4: |[sb,tb]|=x and
A5: not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2);
set qa=|[sb,tb]|;
not (s1<=qa`1 & qa`1<=s2 & t1<=qa`2 & qa`2<=t2) by A5,EUCLID:52;
hence x in {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} by A4;
end;
hence x in {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} iff x in {|[sb,tb]| :
not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by A1;
end;
hence thesis by TARSKI:2;
end;
theorem Th23:
for s1,s2,t1,t2 holds
{ p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2 & t1<p0`2 & p0`2<t2}
is Subset of TOP-REAL 2
proof
let s1,s2,t1,t2;
{ |[ sc,tc ]|: s1<sc & sc<s2 & t1<tc & tc<t2}
is Subset of TOP-REAL 2 by Lm2,Lm7;
hence thesis by Th21;
end;
theorem Th24:
for s1,s2,t1,t2 holds { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} is Subset of TOP-REAL 2
proof
let s1,s2,t1,t2;
{ |[ sb,tb ]|:not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)}
is Subset of TOP-REAL 2 by Lm2,Lm8;
hence thesis by Th22;
end;
theorem Th25:
for s1,t1,s2,t2,P st
P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2} holds P is convex
proof
let s1,t1,s2,t2,P;
assume P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2};
then P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by Th21;
hence thesis by Th8;
end;
theorem Th26:
for s1,t1,s2,t2,P st P = { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} holds P is connected
proof
let s1,t1,s2,t2,P;
assume P= { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)};
then P = {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by Th22;
hence thesis by Th13;
end;
theorem Th27:
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2} holds P is open
proof
let s1,t1,s2,t2;
let P be Subset of TOP-REAL 2;
assume P = { p0 where p0 is Point of TOP-REAL 2:s1<p0`1 & p0`1<s2
& t1<p0`2 & p0`2<t2};
then P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by Th21;
hence thesis by Th18;
end;
theorem Th28:
for s1,t1,s2,t2 for P being Subset of TOP-REAL 2 st
P = { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)} holds P is open
proof
let s1,t1,s2,t2;
let P be Subset of TOP-REAL 2;
assume P= { pq where pq is Point of TOP-REAL 2:
not (s1<=pq`1 & pq`1<=s2 & t1<=pq`2 & pq`2<=t2)};
then P = {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by Th22;
hence thesis by Th19;
end;
theorem Th29:
for s1,t1,s2,t2,P,Q st
P = {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} &
Q = {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)} holds P misses Q
proof
let s1,t1,s2,t2,P,Q;
assume that
A1: P= {p where p is Point of TOP-REAL 2:s1<p`1 & p`1<s2 & t1<p`2 & p`2<t2} and
A2: Q= {qc where qc is Point of TOP-REAL 2:
not (s1<=qc`1 & qc`1<=s2 & t1<=qc`2 & qc`2<=t2)};
A3: P={|[sa,ta]|:s1<sa & sa<s2 & t1<ta & ta<t2} by A1,Th21;
Q= {|[sb,tb]| : not (s1<=sb & sb<=s2 & t1<=tb & tb<=t2)} by A2,Th22;
hence thesis by A3,Th20;
end;
theorem Th30:
for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P`= P1 \/ P2 & P`<> {} & P1 misses P2 &
for P1A,P2B being Subset of (TOP-REAL 2)|P` st P1A = P1 & P2B = P2 holds
P1A is a_component & P2B is a_component
proof
let s1,t1,s2,t2;
let P,P1,P2 be Subset of TOP-REAL 2;
assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P ={p where p is Point of TOP-REAL 2:p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} and
A5: P2 = {pc where pc is Point of TOP-REAL 2:
not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2)};
now
let x be object;
assume
A6: x in P`;
then
A7: not x in P by XBOOLE_0:def 5;
reconsider pd=x as Point of TOP-REAL 2 by A6;
not (pd`1 = s1 & pd`2 <= t2 & pd`2 >= t1 or
pd`1 <= s2 & pd`1 >= s1 & pd`2 = t2 or
pd`1 <= s2 & pd`1 >= s1 & pd`2 = t1 or
pd`1 = s2 & pd`2 <= t2 & pd`2 >= t1)by A3,A7;
then s1<pd`1 & pd`1<s2 & t1 <pd`2 & pd`2 < t2
or not( s1<=pd`1 & pd`1<=s2 & t1<=pd`2 & pd`2<=t2) by XXREAL_0:1;
then x in P1 or x in P2 by A4,A5;
hence x in P1 \/ P2 by XBOOLE_0:def 3;
end;
then
A8: P` c= P1 \/ P2;
now
let x be object such that
A9: x in P1 \/ P2;
now per cases by A9,XBOOLE_0:def 3;
suppose
A10: x in P1;
then
A11: ex pa st pa=x & s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A4;
now
assume x in P;
then ex pb st pb=x &(pb`1 = s1 & pb`2 <= t2 & pb`2 >= t1 or
pb`1 <= s2 & pb`1 >= s1 & pb`2 = t2 or
pb`1 <= s2 & pb`1 >= s1 & pb`2 = t1 or
pb`1 = s2 & pb`2 <= t2 & pb`2 >= t1) by A3;
hence contradiction by A11;
end;
hence x in P` by A10,SUBSET_1:29;
end;
suppose x in P2;
then consider pc being Point of TOP-REAL 2 such that
A12: pc=x and
A13: not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2) by A5;
now
assume pc in P;
then ex p being Point of TOP-REAL 2 st p=pc & (
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1) by A3;
hence contradiction by A1,A2,A13;
end;
hence x in P`by A12,SUBSET_1:29;
end;
end;
hence x in P`;
end;
then
A14: P1 \/ P2 c= P`;
hence
A15: P`=P1 \/ P2 by A8;
set s3 =(s1+s2)/2, t3=(t1+t2)/2;
A16: s1+s1<s1+s2 by A1,XREAL_1:6;
A17: t1+t1<t1+t2 by A2,XREAL_1:6;
A18: (s1+s1)/2<s3 by A16,XREAL_1:74;
A19: (t1+t1)/2<t3 by A17,XREAL_1:74;
A20: s1+s2<s2+s2 by A1,XREAL_1:6;
A21: t1+t2<t2+t2 by A2,XREAL_1:6;
A22: s3<(s2+s2)/2 by A20,XREAL_1:74;
A23: t3<(t2+t2)/2 by A21,XREAL_1:74;
set pp=|[s3,t3]|;
A24: pp`1=s3 by EUCLID:52;
pp`2=t3 by EUCLID:52;
then
A25: |[ s3,t3 ]| in { pp2 where pp2 is Point of TOP-REAL 2:
s1<pp2`1 & pp2`1<s2 & t1<pp2`2 & pp2`2<t2} by A18,A19,A22,A23,A24;
hence
P`<>{} by A4,A14;
set P9 = P`;
P1 misses P2 by A4,A5,Th29;
hence
A26: P1 /\ P2 = {};
now
let P1A,P2B be Subset of (TOP-REAL 2)|P9;
assume that
A27: P1A=P1 and
A28: P2B=P2;
P1 is convex by A4,Th25;
then
A29: P1A is connected by A27,CONNSP_1:23;
A30: P2 is connected by A5,Th26;
A31: P2={ |[ sa,ta ]|:not (s1<=sa & sa<=s2 & t1<=ta & ta<=t2)} by A5,Th22;
reconsider A0={ |[ s3a,t3a ]|:s3a<s1} as Subset of TOP-REAL 2 by Lm2,Lm3;
reconsider A1={ |[ s4,t4 ]|:t4<t1} as Subset of TOP-REAL 2 by Lm2,Lm4;
reconsider A2={ |[ s5,t5 ]|:s2<s5} as Subset of TOP-REAL 2 by Lm2,Lm5;
reconsider A3={ |[ s6,t6 ]|:t2<t6} as Subset of TOP-REAL 2 by Lm2,Lm6;
A32: P2=A0 \/ A1 \/ A2 \/ A3 by A31,Th7;
t2+1>t2 by XREAL_1:29;
then
A33: |[s2+1,t2+1]| in A3;
A34: P2B is connected by A28,A30,CONNSP_1:23;
A35: for CP being Subset of (TOP-REAL 2)|(P9) st
CP is connected holds P1A c= CP implies P1A = CP
proof
let CP be Subset of (TOP-REAL 2)|(P9);
assume CP is connected;
then
A36: ((TOP-REAL 2)|P9)|CP is connected;
now
assume
A37: P1A c= CP;
P1A /\ CP c= CP by XBOOLE_1:17;
then reconsider AP=P1A /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A38: P1 /\ P` =P1A by A15,A27,XBOOLE_1:21;
P1 is open by A4,Th27;
then
A39: P1 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
A40: P`= [#]((TOP-REAL 2)|P9) by PRE_TOPC:def 5;
P1 /\ [#]((TOP-REAL 2)|P9)=P1A by A38,PRE_TOPC:def 5;
then
A41: P1A in the topology of (TOP-REAL 2)|P9 by A39,PRE_TOPC:def 4;
A42: CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
A43: AP<>{}(((TOP-REAL 2)|P9)|CP) by A4,A25,A27,A37,XBOOLE_1:28;
AP in the topology of ((TOP-REAL 2)|P9)|CP by A41,A42,PRE_TOPC:def 4;
then
A44: AP is open by PRE_TOPC:def 2;
P2B /\ CP c= CP by XBOOLE_1:17;
then reconsider BP=P2B /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A45: P2 /\ P` =P2B by A15,A28,XBOOLE_1:21;
P2 is open by A5,Th28;
then
A46: P2 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
P2 /\ [#]((TOP-REAL 2)|P9)=P2B by A45,PRE_TOPC:def 5;
then
A47: P2B in the topology of (TOP-REAL 2)|P9 by A46,PRE_TOPC:def 4;
CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
then BP in the topology of ((TOP-REAL 2)|P9)|CP by A47,PRE_TOPC:def 4;
then
A48: BP is open by PRE_TOPC:def 2;
A49: CP=(P1A \/ P2B) /\ CP by A15,A27,A28,A40,XBOOLE_1:28
.=AP \/ BP by XBOOLE_1:23;
now
assume
A50: BP<>{};
A51: AP /\ BP = P1A /\ (P2B /\ CP) /\ CP by XBOOLE_1:16
.= P1A /\ P2B /\ CP /\ CP by XBOOLE_1:16
.= P1A /\ P2B /\ (CP /\ CP) by XBOOLE_1:16
.= P1A /\ P2B /\ CP;
P1 misses P2 by A4,A5,Th29;
then P1 /\ P2 = {};
then AP misses BP by A27,A28,A51;
hence contradiction by A36,A42,A43,A44,A48,A49,A50,CONNSP_1:11;
end;
hence thesis by A49,XBOOLE_1:28;
end;
hence thesis;
end;
hence P1A is a_component by A29;
for CP being Subset of (TOP-REAL 2)|(P9) st
CP is connected holds P2B c= CP implies P2B = CP
proof
let CP be Subset of (TOP-REAL 2)|(P9);
assume CP is connected;
then
A52: ((TOP-REAL 2)|P9)|CP is connected;
assume
A53: P2B c= CP;
P2B /\ CP c= CP by XBOOLE_1:17;
then reconsider BP=P2B /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A54: P2 /\ P` =P2B by A15,A28,XBOOLE_1:21;
P2 is open by A5,Th28;
then
A55: P2 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
A56: P`= [#]((TOP-REAL 2)|P9) by PRE_TOPC:def 5;
P2 /\ [#]((TOP-REAL 2)|P9)=P2B by A54,PRE_TOPC:def 5;
then
A57: P2B in the topology of (TOP-REAL 2)|P9 by A55,PRE_TOPC:def 4;
A58: CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
A59: BP<>{}(((TOP-REAL 2)|P9)|CP) by A28,A32,A33,A53,XBOOLE_1:28;
BP in the topology of ((TOP-REAL 2)|P9)|CP by A57,A58,PRE_TOPC:def 4;
then
A60: BP is open by PRE_TOPC:def 2;
P1A /\ CP c= CP by XBOOLE_1:17;
then reconsider AP=P1A /\ CP as Subset of ((TOP-REAL 2)|P9)|CP by
PRE_TOPC:8;
A61: P1 /\ P` =P1A by A15,A27,XBOOLE_1:21;
P1 is open by A4,Th27;
then
A62: P1 in the topology of TOP-REAL 2 by PRE_TOPC:def 2;
P1 /\ [#]((TOP-REAL 2)|P9)=P1A by A61,PRE_TOPC:def 5;
then
A63: P1A in the topology of (TOP-REAL 2)|P9 by A62,PRE_TOPC:def 4;
CP=[#](((TOP-REAL 2)|P9)|CP) by PRE_TOPC:def 5;
then AP in the topology of ((TOP-REAL 2)|P9)|CP by A63,PRE_TOPC:def 4;
then
A64: AP is open by PRE_TOPC:def 2;
A65: CP=(P1A \/ P2B) /\ CP by A15,A27,A28,A56,XBOOLE_1:28
.=AP \/ BP by XBOOLE_1:23;
now
assume
A66: AP<>{};
AP /\ BP = P1A /\ (P2B /\ CP) /\ CP by XBOOLE_1:16
.= P1A /\ P2B /\ CP /\ CP by XBOOLE_1:16
.= P1A /\ P2B /\ (CP /\ CP) by XBOOLE_1:16
.= P1A /\ P2B /\ CP;
then AP misses BP by A26,A27,A28;
hence contradiction by A52,A58,A59,A60,A64,A65,A66,CONNSP_1:11;
end;
hence thesis by A53,A65,XBOOLE_1:28;
end;
hence P1A is a_component &
P2B is a_component by A29,A34,A35;
end;
hence thesis;
end;
Lm10: for s1,t1,s2,t2 for P,P1 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} & P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds Cl P1 = P \/ P1
proof
let s1,t1,s2,t2;
let P,P1 be Subset of TOP-REAL 2;
assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
>= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa
`2 & pa`2 < t2};
reconsider P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} as Subset of TOP-REAL 2
by Th24;
A5: P1 c= Cl P1 by PRE_TOPC:18;
reconsider PP = P` as Subset of TOP-REAL 2;
A6: PP=P1 \/ P2 by A1,A2,A3,A4,Th30;
P1 misses P2 by A1,A2,A3,A4,Th30;
then
A7: P1 c= P2` by SUBSET_1:23;
P= (P1 \/ P2)` by A6;
then
A8: P=([#](TOP-REAL 2)\P1) /\ ([#](TOP-REAL 2)\P2) by XBOOLE_1:53;
[#](TOP-REAL 2)=P \/ (P1 \/ P2) by A6,PRE_TOPC:2;
then
A9: [#](TOP-REAL 2)=P \/ P1 \/ P2 by XBOOLE_1:4;
now
let x be object;
assume
A10: x in P2`;
then not x in P2 by XBOOLE_0:def 5;
hence x in P \/ P1 by A9,A10,XBOOLE_0:def 3;
end;
then
A11: P2` c=P \/ P1;
now
let x be object;
assume x in P \/ P1;
then x in P or x in P1 by XBOOLE_0:def 3;
hence x in P2` by A7,A8,XBOOLE_0:def 4;
end;
then P \/ P1 c=P2`;
then
A12: P2`= P \/ P1 by A11;
A13: P2 is open by Th28;
[#](TOP-REAL 2) \ P2` = P2`` .=P2;
then
A14: P \/ P1 is closed by A12,A13,PRE_TOPC:def 3;
A15: P1 c= P \/ P1 by XBOOLE_1:7;
thus Cl P1 c= P \/ P1
by A14,A15,PRE_TOPC:15;
P c= Cl P1
proof
let x be object;
assume x in P;
then consider p being Point of TOP-REAL 2 such that
A16: p=x and
A17: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1 by A3;
reconsider q=p as Point of Euclid 2 by EUCLID:22;
now per cases by A17;
suppose
A18: p`1 = s1 & p`2 <= t2 & p`2 >= t1;
now per cases by A18,XXREAL_0:1;
suppose
A19: p`1 = s1 & p`2 < t2 & p`2 > t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A20: Q is open and
A21: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A20,Lm9,PRE_TOPC:30;
then consider r be Real such that
A22: r>0 and
A23: Ball(q,r) c= Q by A21,TOPMETR:15;
reconsider r as Real;
A24: r/2>0 by A22,XREAL_1:215;
A25: r/2<r by A22,XREAL_1:216;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A26: r2 <= r/2 by XXREAL_0:17;
A27: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
then
A28: r2<=(s2-s1)/2 by A27,XXREAL_0:2;
A29: r2<r by A25,A26,XXREAL_0:2;
A30: s2-s1>0 by A1,XREAL_1:50;
A31: t2-t1>0 by A2,XREAL_1:50;
A32: (s2-s1)/2 >0 by A30,XREAL_1:215;
(t2-t1)/2>0 by A31,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A32,XXREAL_0:15;
then
A33: 0<r2 by A24,XXREAL_0:15;
set pa=|[p`1+r2,p`2]|;
A34: pa`1=p`1+r2 by EUCLID:52;
A35: pa`2=p`2 by EUCLID:52;
(s2-s1)/2<s2-s1 by A30,XREAL_1:216;
then
A36: r2<s2-p`1 by A19,A28,XXREAL_0:2;
A37: s1<pa`1 by A19,A33,A34,XREAL_1:29;
pa`1<s2 by A34,A36,XREAL_1:20;
then
A38: pa in P1 by A4,A19,A35,A37;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A39: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A40: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A39,XREAL_1:7;
(pa`1-p`1)^2=(p`1-pa`1)^2;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A29,A33,A34,A35,SQUARE_1:16;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A40,SQUARE_1:def 2;
then
A41: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A22,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A41,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A23,A38,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
suppose
A42: p`1 = s1 & p`2 = t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A43: Q is open and
A44: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A43,Lm9,PRE_TOPC:30;
then consider r be Real such that
A45: r>0 and
A46: Ball(q,r) c= Q by A44,TOPMETR:15;
reconsider r as Real;
A47: r/2>0 by A45,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A48: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A49: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A50: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A51: r2<=(s2-s1)/2 by A48,A49,XXREAL_0:2;
A52: r2<= (t2-t1)/2 by A48,A50,XXREAL_0:2;
A53: s2-s1>0 by A1,XREAL_1:50;
A54: t2-t1>0 by A2,XREAL_1:50;
A55: (s2-s1)/2 >0 by A53,XREAL_1:215;
(t2-t1)/2>0 by A54,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A55,XXREAL_0:15;
then
A56: 0<r2 by A47,XXREAL_0:15;
set pa=|[p`1+r2,p`2+r2]|;
A57: pa`1=p`1+r2 by EUCLID:52;
A58: pa`2=p`2+r2 by EUCLID:52;
A59: pa`1> s1 by A42,A56,A57,XREAL_1:29;
A60: pa`2> t1 by A42,A56,A58,XREAL_1:29;
(s2-s1)/2<s2-s1 by A53,XREAL_1:216;
then r2<s2-p`1 by A42,A51,XXREAL_0:2;
then
A61: pa`1<s2 by A57,XREAL_1:20;
(t2-t1)/2<t2-t1 by A54,XREAL_1:216;
then r2<t2-p`2 by A42,A52,XXREAL_0:2;
then pa`2<t2 by A58,XREAL_1:20;
then
A62: pa in P1 by A4,A59,A60,A61;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A63: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A64: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A63,XREAL_1:7;
(pa`1-p`1)^2=(p`1-pa`1)^2;
then (p`1 - pa`1)^2 <= (r/2)^2 by A56,A57,SQUARE_1:15,XXREAL_0:17;
then
A65: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A57,A58,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A45,A47,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A65,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A64,SQUARE_1:def 2;
then
A66: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A45,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A66,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A46,A62,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
suppose
A67: p`1 = s1 & p`2 = t2;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A68: Q is open and
A69: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A68,Lm9,PRE_TOPC:30;
then consider r be Real such that
A70: r>0 and
A71: Ball(q,r) c= Q by A69,TOPMETR:15;
reconsider r as Real;
A72: r/2>0 by A70,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A73: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A74: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A75: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A76: r2<=(s2-s1)/2 by A73,A74,XXREAL_0:2;
A77: r2<= (t2-t1)/2 by A73,A75,XXREAL_0:2;
A78: s2-s1>0 by A1,XREAL_1:50;
A79: t2-t1>0 by A2,XREAL_1:50;
A80: (s2-s1)/2 >0 by A78,XREAL_1:215;
(t2-t1)/2>0 by A79,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A80,XXREAL_0:15;
then
A81: 0<r2 by A72,XXREAL_0:15;
set pa=|[p`1+r2,p`2-r2]|;
A82: pa`1=p`1+r2 by EUCLID:52;
A83: pa`2=p`2-r2 by EUCLID:52;
A84: pa`1> s1 by A67,A81,A82,XREAL_1:29;
A85: pa`2< t2 by A67,A81,A83,XREAL_1:44;
(s2-s1)/2<s2-s1 by A78,XREAL_1:216;
then r2<s2-p`1 by A67,A76,XXREAL_0:2;
then
A86: pa`1<s2 by A82,XREAL_1:20;
(t2-t1)/2<t2-t1 by A79,XREAL_1:216;
then r2<p`2-t1 by A67,A77,XXREAL_0:2;
then pa`2>t1 by A83,XREAL_1:12;
then
A87: pa in P1 by A4,A84,A85,A86;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A88: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A89: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A88,XREAL_1:7;
r2^2<= (r/2)^2 by A81,SQUARE_1:15,XXREAL_0:17;
then
A90: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A82,A83,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A70,A72,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A90,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A89,SQUARE_1:def 2;
then
A91: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A70,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A91,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A71,A87,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
end;
hence thesis by A16;
end;
suppose
A92: p`1 <= s2 & p`1 >= s1 & p`2 = t2;
now per cases by A92,XXREAL_0:1;
suppose
A93: p`2 = t2 & p`1 < s2 & p`1 > s1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A94: Q is open and
A95: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A94,Lm9,PRE_TOPC:30;
then consider r be Real such that
A96: r>0 and
A97: Ball(q,r) c= Q by A95,TOPMETR:15;
reconsider r as Real;
A98: r/2>0 by A96,XREAL_1:215;
A99: r/2<r by A96,XREAL_1:216;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A100: r2 <= r/2 by XXREAL_0:17;
A101: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
then
A102: r2<= (t2-t1)/2 by A101,XXREAL_0:2;
A103: r2<r by A99,A100,XXREAL_0:2;
A104: s2-s1>0 by A1,XREAL_1:50;
A105: t2-t1>0 by A2,XREAL_1:50;
A106: (s2-s1)/2 >0 by A104,XREAL_1:215;
(t2-t1)/2>0 by A105,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A106,XXREAL_0:15;
then
A107: 0<r2 by A98,XXREAL_0:15;
set pa=|[p`1,p`2-r2]|;
A108: pa`1=p`1 by EUCLID:52;
A109: pa`2=p`2-r2 by EUCLID:52;
(t2-t1)/2<t2-t1 by A105,XREAL_1:216;
then r2<p`2-t1 by A93,A102,XXREAL_0:2;
then
A110: t1 <pa`2 by A109,XREAL_1:12;
pa`2 < t2 by A93,A107,A109,XREAL_1:44;
then
A111: pa in P1 by A4,A93,A108,A110;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A112: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A113: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A112,XREAL_1:7;
(p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A103,A107,A108,A109,SQUARE_1:16;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A113,SQUARE_1:def 2;
then
A114: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A96,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A114,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A97,A111,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
suppose
A115: p`2 = t2 & p`1 = s1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A116: Q is open and
A117: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A116,Lm9,PRE_TOPC:30;
then consider r be Real such that
A118: r>0 and
A119: Ball(q,r) c= Q by A117,TOPMETR:15;
reconsider r as Real;
A120: r/2>0 by A118,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A121: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A122: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A123: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A124: r2<=(s2-s1)/2 by A121,A122,XXREAL_0:2;
A125: r2<= (t2-t1)/2 by A121,A123,XXREAL_0:2;
A126: s2-s1>0 by A1,XREAL_1:50;
A127: t2-t1>0 by A2,XREAL_1:50;
A128: (s2-s1)/2 >0 by A126,XREAL_1:215;
(t2-t1)/2>0 by A127,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A128,XXREAL_0:15;
then
A129: 0<r2 by A120,XXREAL_0:15;
set pa=|[p`1+r2,p`2-r2]|;
A130: pa`1=p`1+r2 by EUCLID:52;
A131: pa`2=p`2-r2 by EUCLID:52;
A132: pa`1> s1 by A115,A129,A130,XREAL_1:29;
A133: pa`2< t2 by A115,A129,A131,XREAL_1:44;
(t2-t1)/2<t2-t1 by A127,XREAL_1:216;
then r2<p`2-t1 by A115,A125,XXREAL_0:2;
then
A134: pa`2>t1 by A131,XREAL_1:12;
(s2-s1)/2<s2-s1 by A126,XREAL_1:216;
then r2<s2-p`1 by A115,A124,XXREAL_0:2;
then pa`1<s2 by A130,XREAL_1:20;
then
A135: pa in P1 by A4,A132,A133,A134;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A136: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A137: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A136,XREAL_1:7;
(p`2 - pa`2)^2 <= (r/2)^2 by A129,A131,SQUARE_1:15,XXREAL_0:17;
then
A138: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A130,A131,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A118,A120,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A138,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A137,SQUARE_1:def 2;
then
A139: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A118,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A139,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A119,A135,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
suppose
A140: p`2 = t2 & p`1 = s2;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A141: Q is open and
A142: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A141,Lm9,PRE_TOPC:30;
then consider r be Real such that
A143: r>0 and
A144: Ball(q,r) c= Q by A142,TOPMETR:15;
reconsider r as Real;
A145: r/2>0 by A143,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A146: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A147: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A148: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A149: r2<=(s2-s1)/2 by A146,A147,XXREAL_0:2;
A150: r2<= (t2-t1)/2 by A146,A148,XXREAL_0:2;
A151: s2-s1>0 by A1,XREAL_1:50;
A152: t2-t1>0 by A2,XREAL_1:50;
A153: (s2-s1)/2 >0 by A151,XREAL_1:215;
(t2-t1)/2>0 by A152,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A153,XXREAL_0:15;
then
A154: 0<r2 by A145,XXREAL_0:15;
set pa=|[p`1-r2,p`2-r2]|;
A155: pa`1=p`1-r2 by EUCLID:52;
A156: pa`2=p`2-r2 by EUCLID:52;
A157: pa`1< s2 by A140,A154,A155,XREAL_1:44;
A158: pa`2< t2 by A140,A154,A156,XREAL_1:44;
(s2-s1)/2<s2-s1 by A151,XREAL_1:216;
then r2<p`1-s1 by A140,A149,XXREAL_0:2;
then
A159: pa`1>s1 by A155,XREAL_1:12;
(t2-t1)/2<t2-t1 by A152,XREAL_1:216;
then r2<p`2-t1 by A140,A150,XXREAL_0:2;
then pa`2>t1 by A156,XREAL_1:12;
then
A160: pa in P1 by A4,A157,A158,A159;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A161: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A162: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A161,XREAL_1:7;
r2^2<= (r/2)^2 by A154,SQUARE_1:15,XXREAL_0:17;
then
A163: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A155,A156,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A143,A145,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A163,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A162,SQUARE_1:def 2;
then
A164: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A143,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A164,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A144,A160,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
end;
hence thesis by A16;
end;
suppose
A165: p`1 <= s2 & p`1 >= s1 & p`2 = t1;
now per cases by A165,XXREAL_0:1;
suppose
A166: p`2 = t1 & p`1 < s2 & p`1 > s1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A167: Q is open and
A168: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A167,Lm9,PRE_TOPC:30;
then consider r be Real such that
A169: r>0 and
A170: Ball(q,r) c= Q by A168,TOPMETR:15;
reconsider r as Real;
A171: r/2>0 by A169,XREAL_1:215;
A172: r/2<r by A169,XREAL_1:216;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A173: r2 <= r/2 by XXREAL_0:17;
A174: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
then
A175: r2<= (t2-t1)/2 by A174,XXREAL_0:2;
A176: r2<r by A172,A173,XXREAL_0:2;
A177: s2-s1>0 by A1,XREAL_1:50;
A178: t2-t1>0 by A2,XREAL_1:50;
A179: (s2-s1)/2 >0 by A177,XREAL_1:215;
(t2-t1)/2>0 by A178,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A179,XXREAL_0:15;
then
A180: 0<r2 by A171,XXREAL_0:15;
set pa=|[p`1,p`2+r2]|;
A181: pa`2=p`2+r2 by EUCLID:52;
A182: pa`1=p`1 by EUCLID:52;
(t2-t1)/2<t2-t1 by A178,XREAL_1:216;
then
A183: r2<t2-p`2 by A166,A175,XXREAL_0:2;
A184: t1 <pa`2 by A166,A180,A181,XREAL_1:29;
pa`2 < t2 by A181,A183,XREAL_1:20;
then
A185: pa in P1 by A4,A166,A182,A184;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A186: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A187: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A186,XREAL_1:7;
(pa`2-p`2)^2=(p`2-pa`2)^2;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A176,A180,A181,A182
,SQUARE_1:16;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A187,SQUARE_1:def 2;
then
A188: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A169,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A188,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A170,A185,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
suppose
A189: p`2 = t1 & p`1 = s1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A190: Q is open and
A191: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A190,Lm9,PRE_TOPC:30;
then consider r be Real such that
A192: r>0 and
A193: Ball(q,r) c= Q by A191,TOPMETR:15;
reconsider r as Real;
A194: r/2>0 by A192,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A195: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A196: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A197: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A198: r2<=(s2-s1)/2 by A195,A196,XXREAL_0:2;
A199: r2<= (t2-t1)/2 by A195,A197,XXREAL_0:2;
A200: s2-s1>0 by A1,XREAL_1:50;
A201: t2-t1>0 by A2,XREAL_1:50;
A202: (s2-s1)/2 >0 by A200,XREAL_1:215;
(t2-t1)/2>0 by A201,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A202,XXREAL_0:15;
then
A203: 0<r2 by A194,XXREAL_0:15;
set pa=|[p`1+r2,p`2+r2]|;
A204: pa`1=p`1+r2 by EUCLID:52;
A205: pa`2=p`2+r2 by EUCLID:52;
A206: pa`1> s1 by A189,A203,A204,XREAL_1:29;
A207: pa`2> t1 by A189,A203,A205,XREAL_1:29;
(s2-s1)/2<s2-s1 by A200,XREAL_1:216;
then r2<s2-p`1 by A189,A198,XXREAL_0:2;
then
A208: pa`1<s2 by A204,XREAL_1:20;
(t2-t1)/2<t2-t1 by A201,XREAL_1:216;
then r2<t2-p`2 by A189,A199,XXREAL_0:2;
then pa`2<t2 by A205,XREAL_1:20;
then
A209: pa in P1 by A4,A206,A207,A208;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A210: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A211: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A210,XREAL_1:7;
(pa`1-p`1)^2=(p`1-pa`1)^2;
then (p`1 - pa`1)^2 <= (r/2)^2 by A203,A204,SQUARE_1:15,XXREAL_0:17;
then
A212: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A204,A205,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A192,A194,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A212,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A211,SQUARE_1:def 2;
then
A213: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A192,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A213,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A193,A209,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
suppose
A214: p`2 = t1 & p`1 = s2;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A215: Q is open and
A216: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A215,Lm9,PRE_TOPC:30;
then consider r be Real such that
A217: r>0 and
A218: Ball(q,r) c= Q by A216,TOPMETR:15;
reconsider r as Real;
A219: r/2>0 by A217,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A220: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A221: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A222: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A223: r2<=(s2-s1)/2 by A220,A221,XXREAL_0:2;
A224: r2<= (t2-t1)/2 by A220,A222,XXREAL_0:2;
A225: s2-s1>0 by A1,XREAL_1:50;
A226: t2-t1>0 by A2,XREAL_1:50;
A227: (s2-s1)/2 >0 by A225,XREAL_1:215;
(t2-t1)/2>0 by A226,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A227,XXREAL_0:15;
then
A228: 0<r2 by A219,XXREAL_0:15;
set pa=|[p`1-r2,p`2+r2]|;
A229: pa`1=p`1-r2 by EUCLID:52;
A230: pa`2=p`2+r2 by EUCLID:52;
then
A231: pa`2> t1 by A214,A228,XREAL_1:29;
A232: pa`1< s2 by A214,A228,A229,XREAL_1:44;
(t2-t1)/2<t2-t1 by A226,XREAL_1:216;
then r2<t2-p`2 by A214,A224,XXREAL_0:2;
then
A233: pa`2<t2 by A230,XREAL_1:20;
(s2-s1)/2<s2-s1 by A225,XREAL_1:216;
then r2<p`1-s1 by A214,A223,XXREAL_0:2;
then pa`1>s1 by A229,XREAL_1:12;
then
A234: pa in P1 by A4,A231,A232,A233;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A235: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A236: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A235,XREAL_1:7;
r2^2<= (r/2)^2 by A228,SQUARE_1:15,XXREAL_0:17;
then
A237: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A229,A230,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A217,A219,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A237,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A236,SQUARE_1:def 2;
then
A238: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A217,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A238,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A218,A234,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
end;
hence thesis by A16;
end;
suppose
A239: p`1 = s2 & p`2 <= t2 & p`2 >= t1;
now per cases by A239,XXREAL_0:1;
suppose
A240: p`1 = s2 & p`2 < t2 & p`2 > t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A241: Q is open and
A242: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A241,Lm9,PRE_TOPC:30;
then consider r being Real such that
A243: r>0 and
A244: Ball(q,r) c= Q by A242,TOPMETR:15;
reconsider r as Real;
A245: r/2>0 by A243,XREAL_1:215;
A246: r/2<r by A243,XREAL_1:216;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A247: r2 <= r/2 by XXREAL_0:17;
A248: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
then
A249: r2<=(s2-s1)/2 by A248,XXREAL_0:2;
A250: r2<r by A246,A247,XXREAL_0:2;
A251: s2-s1>0 by A1,XREAL_1:50;
A252: t2-t1>0 by A2,XREAL_1:50;
A253: (s2-s1)/2 >0 by A251,XREAL_1:215;
(t2-t1)/2>0 by A252,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A253,XXREAL_0:15;
then
A254: 0<r2 by A245,XXREAL_0:15;
set pa=|[p`1-r2,p`2]|;
A255: pa`2=p`2 by EUCLID:52;
A256: pa`1=p`1-r2 by EUCLID:52;
(s2-s1)/2<s2-s1 by A251,XREAL_1:216;
then r2<p`1-s1 by A240,A249,XXREAL_0:2;
then
A257: s1<pa`1 by A256,XREAL_1:12;
pa`1<s2 by A240,A254,A256,XREAL_1:44;
then
A258: pa in P1 by A4,A240,A255,A257;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A259: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A260: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A259,XREAL_1:7;
(p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A250,A254,A255,A256,SQUARE_1:16;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A260,SQUARE_1:def 2;
then
A261: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A243,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A261,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A244,A258,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
suppose
A262: p`1 = s2 & p`2 = t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A263: Q is open and
A264: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A263,Lm9,PRE_TOPC:30;
then consider r being Real such that
A265: r>0 and
A266: Ball(q,r) c= Q by A264,TOPMETR:15;
reconsider r as Real;
A267: r/2>0 by A265,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A268: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A269: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A270: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A271: r2<=(s2-s1)/2 by A268,A269,XXREAL_0:2;
A272: r2<= (t2-t1)/2 by A268,A270,XXREAL_0:2;
A273: s2-s1>0 by A1,XREAL_1:50;
A274: t2-t1>0 by A2,XREAL_1:50;
A275: (s2-s1)/2 >0 by A273,XREAL_1:215;
(t2-t1)/2>0 by A274,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A275,XXREAL_0:15;
then
A276: 0<r2 by A267,XXREAL_0:15;
set pa=|[p`1-r2,p`2+r2]|;
A277: pa`2=p`2+r2 by EUCLID:52;
A278: pa`1=p`1-r2 by EUCLID:52;
A279: pa`2> t1 by A262,A276,A277,XREAL_1:29;
A280: pa`1< s2 by A262,A276,A278,XREAL_1:44;
(s2-s1)/2<s2-s1 by A273,XREAL_1:216;
then r2<p`1-s1 by A262,A271,XXREAL_0:2;
then
A281: pa`1>s1 by A278,XREAL_1:12;
(t2-t1)/2<t2-t1 by A274,XREAL_1:216;
then r2<t2-p`2 by A262,A272,XXREAL_0:2;
then pa`2<t2 by A277,XREAL_1:20;
then
A282: pa in P1 by A4,A279,A280,A281;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A283: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A284: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A283,XREAL_1:7;
(p`1 - pa`1)^2 <= (r/2)^2 by A276,A278,SQUARE_1:15,XXREAL_0:17;
then
A285: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A277,A278,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A265,A267,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A285,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A284,SQUARE_1:def 2;
then
A286: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A265,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A286,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A266,A282,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
suppose
A287: p`1 = s2 & p`2 = t2;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P1 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A288: Q is open and
A289: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A288,Lm9,PRE_TOPC:30;
then consider r being Real such that
A290: r>0 and
A291: Ball(q,r) c= Q by A289,TOPMETR:15;
reconsider r as Real;
A292: r/2>0 by A290,XREAL_1:215;
set r2=min(r/2,min((s2-s1)/2,(t2-t1)/2));
A293: r2<=min((s2-s1)/2,(t2-t1)/2) by XXREAL_0:17;
A294: min((s2-s1)/2,(t2-t1)/2) <=(s2-s1)/2 by XXREAL_0:17;
A295: min((s2-s1)/2,(t2-t1)/2)<= (t2-t1)/2 by XXREAL_0:17;
A296: r2<=(s2-s1)/2 by A293,A294,XXREAL_0:2;
A297: r2<= (t2-t1)/2 by A293,A295,XXREAL_0:2;
A298: s2-s1>0 by A1,XREAL_1:50;
A299: t2-t1>0 by A2,XREAL_1:50;
A300: (s2-s1)/2 >0 by A298,XREAL_1:215;
(t2-t1)/2>0 by A299,XREAL_1:215;
then 0<min((s2-s1)/2,(t2-t1)/2) by A300,XXREAL_0:15;
then
A301: 0<r2 by A292,XXREAL_0:15;
set pa=|[p`1-r2,p`2-r2]|;
A302: pa`1=p`1-r2 by EUCLID:52;
A303: pa`2=p`2-r2 by EUCLID:52;
A304: pa`1< s2 by A287,A301,A302,XREAL_1:44;
A305: pa`2< t2 by A287,A301,A303,XREAL_1:44;
(s2-s1)/2<s2-s1 by A298,XREAL_1:216;
then r2<p`1-s1 by A287,A296,XXREAL_0:2;
then
A306: pa`1>s1 by A302,XREAL_1:12;
(t2-t1)/2<t2-t1 by A299,XREAL_1:216;
then r2<p`2-t1 by A287,A297,XXREAL_0:2;
then pa`2>t1 by A303,XREAL_1:12;
then
A307: pa in P1 by A4,A304,A305,A306;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A308: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A309: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A308,XREAL_1:7;
r2^2<= (r/2)^2 by A301,SQUARE_1:15,XXREAL_0:17;
then
A310: (
p`1 - pa`1)^2 + (p`2 - pa`2)^2 <= (r/2)^2 +(r /2)^2
by A302,A303,XREAL_1:7;
r^2=(r/2)^2+(r/2)^2+2*(r/2)*(r/2);
then r^2>(r/2)^2+(r/2)^2 by A290,A292,XREAL_1:29,129;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A310,XXREAL_0:2;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A309,SQUARE_1:def 2;
then
A311: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A290,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A311,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A291,A307,XBOOLE_0:3;
end;
hence p in Cl P1 by PRE_TOPC:def 7;
end;
end;
hence thesis by A16;
end;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_1:8;
end;
Lm11: for s1,t1,s2,t2 for P,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} & P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds Cl P2 = P \/ P2
proof
let s1,t1,s2,t2;
let P,P2 be Subset of TOP-REAL 2;
assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
>= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
t1<=pb`2 & pb`2<=t2)};
A5: P2 c= Cl P2 by PRE_TOPC:18;
reconsider P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} as Subset of TOP-REAL 2 by Th23;
reconsider PP = P` as Subset of TOP-REAL 2;
A6: PP=P1 \/ P2 by A1,A2,A3,A4,Th30;
P1 misses P2 by A1,A2,A3,A4,Th30;
then
A7: P2 c= P1` by SUBSET_1:23;
P= (P1 \/ P2)` by A6;
then
A8: P=([#](TOP-REAL 2)\P1) /\ ([#](TOP-REAL 2)\P2) by XBOOLE_1:53;
A9: [#](TOP-REAL 2)=P \/ (P2 \/ P1) by A6,PRE_TOPC:2
.=P \/ P2 \/ P1 by XBOOLE_1:4;
now
let x be object;
assume
A10: x in P1`;
then not x in P1 by XBOOLE_0:def 5;
hence x in P \/ P2 by A9,A10,XBOOLE_0:def 3;
end;
then
A11: P1` c=P \/ P2;
now
let x be object;
assume x in P \/ P2;
then x in P or x in P2 by XBOOLE_0:def 3;
hence x in P1` by A7,A8,XBOOLE_0:def 4;
end;
then P \/ P2 c=P1`;
then
A12: P1`= P \/ P2 by A11;
A13: P1 is open by Th27;
[#](TOP-REAL 2) \ P1` = P1`` .=P1;
then
A14: P \/ P2 is closed by A12,A13,PRE_TOPC:def 3;
A15: P2 c= P \/ P2 by XBOOLE_1:7;
thus Cl P2 c= P \/ P2
by A14,A15,PRE_TOPC:15;
P c= Cl P2
proof
let x be object;
assume x in P;
then consider p being Point of TOP-REAL 2 such that
A16: p=x and
A17: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1 by A3;
reconsider q=p as Point of Euclid 2 by EUCLID:22;
now per cases by A17;
suppose
A18: p`1 = s1 & p`2 <= t2 & p`2 >= t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P2 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A19: Q is open and
A20: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A19,Lm9,PRE_TOPC:30;
then consider r be Real such that
A21: r>0 and
A22: Ball(q,r) c= Q by A20,TOPMETR:15;
reconsider r as Real;
set pa=|[p`1-r/2,p`2]|;
A23: pa`1=p`1-r/2 by EUCLID:52;
A24: pa`2=p`2 by EUCLID:52;
A25: r/2>0 by A21,XREAL_1:215;
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A18,A21,A23,
XREAL_1:44,215;
then
A26: pa in P2 by A4;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A27: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A28: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A27,XREAL_1:7;
p`1 - pa`1 < r by A21,A23,XREAL_1:216;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A23,A24,A25,SQUARE_1:16
;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A28,SQUARE_1:def 2;
then
A29: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A21,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A29,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
then P2 /\ Q <> {} by A22,A26,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by A16,PRE_TOPC:def 7;
end;
suppose
A30: p`1 <= s2 & p`1 >= s1 & p`2 = t2;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P2 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A31: Q is open and
A32: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A31,Lm9,PRE_TOPC:30;
then consider r being Real such that
A33: r>0 and
A34: Ball(q,r) c= Q by A32,TOPMETR:15;
reconsider r as Real;
set pa=|[p`1,p`2+r/2]|;
A35: pa`1=p`1 by EUCLID:52;
A36: pa`2=p`2+r/2 by EUCLID:52;
A37: r/2>0 by A33,XREAL_1:215;
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A30,A33,A36,
XREAL_1:29,215;
then
A38: pa in P2 by A4;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A39: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A40: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A39,XREAL_1:7;
A41: pa`2 - p`2 < r by A33,A36,XREAL_1:216;
(pa`2-p`2)^2=(p`2-pa`2)^2;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A35,A36,A37,A41,SQUARE_1:16;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A40,SQUARE_1:def 2;
then
A42: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A33,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A42,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
then P2 /\ Q <> {} by A34,A38,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by A16,PRE_TOPC:def 7;
end;
suppose
A43: p`1 <= s2 & p`1 >= s1 & p`2 = t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P2 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A44: Q is open and
A45: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A44,Lm9,PRE_TOPC:30;
then consider r being Real such that
A46: r>0 and
A47: Ball(q,r) c= Q by A45,TOPMETR:15;
reconsider r as Real;
set pa=|[p`1,p`2-r/2]|;
A48: pa`1=p`1 by EUCLID:52;
A49: pa`2=p`2-r/2 by EUCLID:52;
A50: r/2>0 by A46,XREAL_1:215;
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2)
by A43,A46,A49,XREAL_1:44,215;
then
A51: pa in P2 by A4;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A52: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A53: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A52,XREAL_1:7;
p`2 - pa`2 < r by A46,A49,XREAL_1:216;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2 by A48,A49,A50,SQUARE_1:16
;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A53,SQUARE_1:def 2;
then
A54: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A46,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A54,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A47,A51,XBOOLE_0:3;
end;
hence thesis by A16,PRE_TOPC:def 7;
end;
suppose
A55: p`1 = s2 & p`2 <= t2 & p`2 >= t1;
for Q being Subset of TOP-REAL 2 st Q is open holds
p in Q implies P2 meets Q
proof
let Q be Subset of TOP-REAL 2;
assume that
A56: Q is open and
A57: p in Q;
reconsider QQ = Q as Subset of TopSpaceMetr Euclid 2 by Lm9;
QQ is open by A56,Lm9,PRE_TOPC:30;
then consider r being Real such that
A58: r>0 and
A59: Ball(q,r) c= Q by A57,TOPMETR:15;
reconsider r as Real;
set pa=|[p`1+r/2,p`2]|;
A60: pa`1=p`1+r/2 by EUCLID:52;
A61: pa`2=p`2 by EUCLID:52;
A62: r/2>0 by A58,XREAL_1:215;
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2)
by A55,A58,A60,XREAL_1:29,215;
then
A63: pa in P2 by A4;
reconsider qa=pa as Point of Euclid 2 by EUCLID:22;
A64: 0 <= (p`1 - pa`1)^2 by XREAL_1:63;
0 <= (p`2 - pa`2)^2 by XREAL_1:63;
then
A65: 0+0 <= (p`1 - pa`1)^2 + (p`2 - pa`2)^2 by A64,XREAL_1:7;
A66: pa`1 - p`1 < r by A58,A60,XREAL_1:216;
(pa`1-p`1)^2=(p`1-pa`1)^2;
then (p`1 - pa`1)^2 + (p`2 - pa`2)^2 < r^2
by A60,A61,A62,A66,SQUARE_1:16;
then (sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2))^2<r^2
by A65,SQUARE_1:def 2;
then
A67: sqrt ((p`1 - pa`1)^2 + (p`2 - pa`2)^2) <r by A58,SQUARE_1:15;
(Pitag_dist 2).(q,qa)=dist(q,qa) by METRIC_1:def 1;
then dist(q,qa)<r by A67,TOPREAL3:7;
then pa in Ball(q,r) by METRIC_1:11;
hence thesis by A59,A63,XBOOLE_0:3;
end;
hence thesis by A16,PRE_TOPC:def 7;
end;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_1:8;
end;
theorem Th31:
for s1,t1,s2,t2 for P,P1,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)}
holds P = (Cl P1) \ P1 & P = (Cl P2) \P2
proof
let s1,t1,s2,t2;
let P,P1,P2 be Subset of TOP-REAL 2;
assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
>= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P1 = {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa
`2 & pa`2 < t2} and
A5: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
t1<=pb`2 & pb`2<=t2)};
reconsider PP = P` as Subset of TOP-REAL 2;
PP=P1 \/ P2 by A1,A2,A3,A4,A5,Th30;
then P= (P1 \/ P2)`;
then
A6: P=([#](TOP-REAL 2)\P1) /\ ([#](TOP-REAL 2)\P2) by XBOOLE_1:53;
then
A7: P c=[#](TOP-REAL 2)\P2 by XBOOLE_1:17;
A8: Cl P2 = P \/ P2 by A1,A2,A3,A5,Lm11;
A9: (P \/ P2) \ P2 c= P
proof
let x be object;
assume
A10: x in (P \/ P2) \ P2;
then
A11: x in P \/ P2 by XBOOLE_0:def 5;
not x in P2 by A10,XBOOLE_0:def 5;
hence thesis by A11,XBOOLE_0:def 3;
end;
P c= Cl P2 by A8,XBOOLE_1:7;
then P c= Cl P2 /\ P2` by A7,XBOOLE_1:19;
then
A12: P c= (Cl P2)\P2 by SUBSET_1:13;
A13: P c=[#](TOP-REAL 2)\P1 by A6,XBOOLE_1:17;
A14: Cl P1 = P \/ P1 by A1,A2,A3,A4,Lm10;
A15: (P \/ P1) \ P1 c= P
proof
let x be object;
assume
A16: x in (P \/ P1) \ P1;
then
A17: x in P \/ P1 by XBOOLE_0:def 5;
not x in P1 by A16,XBOOLE_0:def 5;
hence thesis by A17,XBOOLE_0:def 3;
end;
P c= Cl P1 by A14,XBOOLE_1:7;
then P c= Cl P1 /\ P1` by A13,XBOOLE_1:19;
then P c= (Cl P1)\P1 by SUBSET_1:13;
hence thesis by A8,A9,A12,A14,A15;
end;
theorem Th32:
for s1,s2,t1,t2,P,P1 st P = { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds P1 c= [#] ((TOP-REAL 2)|P`)
proof
let s1,s2,t1,t2,P,P1;
assume that
A1: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1
or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1
= s2 & p`2 <= t2 & p`2 >= t1} and
A2: P1 = {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa
`2 & pa`2 < t2};
let x be object;
assume
A3: x in P1;
then
A4: ex pa being Point of TOP-REAL 2 st pa=x &
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2 by A2;
now
assume x in { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
then ex p being Point of TOP-REAL 2 st p=x & (
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1);
hence contradiction by A4;
end;
then x in P` by A1,A3,SUBSET_1:29;
hence thesis by PRE_TOPC:def 5;
end;
theorem
for s1,s2,t1,t2,P,P1 st P = { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds
P1 is Subset of (TOP-REAL 2)|P`
proof
let s1,s2,t1,t2,P,P1;
assume that
A1: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1
or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1
= s2 & p`2 <= t2 & p`2 >= t1} and
A2: P1 = {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa
`2 & pa`2 < t2};
P1 c= [#]((TOP-REAL 2)|P`)by A1,A2,Th32;
hence thesis;
end;
theorem Th34:
for s1,s2,t1,t2,P,P2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P2 c= [#]((TOP-REAL 2)|P`)
proof
let s1,s2,t1,t2,P,P2;
assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
>= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
t1<=pb`2 & pb`2<=t2)};
let x be object;
assume
A5: x in P2;
then
A6: ex pa being Point of TOP-REAL 2 st pa=x &
not( s1<=pa`1 & pa`1<=s2 & t1<=pa`2 & pa`2<=t2) by A4;
now
assume x in { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
then ex p being Point of TOP-REAL 2 st p=x & (
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1);
hence contradiction by A1,A2,A6;
end;
then x in P` by A3,A5,SUBSET_1:29;
hence thesis by PRE_TOPC:def 5;
end;
theorem
for s1,s2,t1,t2,P,P2 st s1<s2 & t1< t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)} holds
P2 is Subset of (TOP-REAL 2)|P`
proof
let s1,s2,t1,t2,P,P2;
assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2
>= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1
or p`1 = s2 & p`2 <= t2 & p`2 >= t1} and
A4: P2 = {pb where pb is Point of TOP-REAL 2: not( s1<=pb`1 & pb`1<=s2 &
t1<=pb`2 & pb`2<=t2)};
P2 c= [#]((TOP-REAL 2)|P`) by A1,A2,A3,A4,Th34;
hence thesis;
end;
begin
::
:: The Jordan's property
::
definition
let S be Subset of TOP-REAL 2;
attr S is Jordan means
S`<> {} & ex A1,A2 being Subset of TOP-REAL 2 st
S` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 &
for C1,C2 being Subset of (TOP-REAL 2)|S` st C1 = A1 & C2 = A2 holds
C1 is a_component & C2 is a_component;
end;
theorem
for S being Subset of TOP-REAL 2 st S is Jordan holds S`<> {} &
ex A1,A2 being Subset of TOP-REAL 2 st
ex C1,C2 being Subset of (TOP-REAL 2)|S` st S` = A1 \/ A2 & A1 misses A2 &
(Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 &
C1 is a_component & C2 is a_component &
for C3 being Subset of (TOP-REAL 2)|S` st C3 is a_component holds
C3 = C1 or C3 = C2
proof
let S be Subset of TOP-REAL 2;
assume
A1: S is Jordan;
then reconsider S9 = S` as non empty Subset of TOP-REAL 2;
consider A1,A2 being Subset of TOP-REAL 2 such that
A2: S`=A1 \/ A2 and
A3: A1 misses A2 and
A4: (Cl A1)\A1=(Cl A2)\A2 and
A5: for C1,C2 being Subset of (TOP-REAL 2)|S`
st C1=A1 & C2=A2 holds C1 is a_component & C2 is a_component by A1;
A6: A1 c= S` by A2,XBOOLE_1:7;
A7: A2 c= S` by A2,XBOOLE_1:7;
A8: [#]((TOP-REAL 2)|S`)=S` by PRE_TOPC:def 5;
A1 c= [#]((TOP-REAL 2)|S`) by A6,PRE_TOPC:def 5;
then reconsider G0A=A1,G0B=A2 as Subset of (TOP-REAL 2)|S9 by A7,
PRE_TOPC:def 5;
A9: G0A=A1;
G0B=A2;
then
A10: G0A is a_component by A5;
A11: G0B is a_component by A5,A9;
now
let C3 be Subset of (TOP-REAL 2)|S9;
assume
A12: C3 is a_component;
then
A13: C3 <>{}((TOP-REAL 2)|S9) by CONNSP_1:32;
C3 /\(G0A \/ G0B)=C3 by A2,A8,XBOOLE_1:28;
then
A14: (C3 /\ G0A) \/ (C3 /\ G0B) <>{} by A13,XBOOLE_1:23;
now per cases by A14;
suppose C3 /\ G0A<>{};
then
A15: C3 meets G0A;
A16: C3 is connected by A12;
A17: G0A is connected by A10;
then
A18: C3 \/ G0A is connected by A15,A16,CONNSP_1:1,17;
G0A c= C3 \/ G0A by XBOOLE_1:7;
then G0A=C3 \/ G0A by A10,A18;
then C3 c= G0A by XBOOLE_1:7;
hence C3=G0A or C3=G0B by A12,A17;
end;
suppose C3 /\ A2<>{};
then
A19: C3 meets G0B;
A20: C3 is connected by A12;
A21: G0B is connected by A11;
then
A22: C3 \/ G0B is connected by A19,A20,CONNSP_1:1,17;
G0B c= C3 \/ G0B by XBOOLE_1:7;
then G0B=C3 \/ G0B by A11,A22;
then C3 c= G0B by XBOOLE_1:7;
hence C3=G0A or C3=G0B by A12,A21;
end;
end;
hence C3=G0A or C3=G0B;
end;
hence thesis by A2,A3,A4,A10,A11;
end;
theorem
for s1,s2,t1,t2 for P being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} holds P is Jordan
proof
let s1,s2,t1,t2;
let P be Subset of TOP-REAL 2;
assume that
A1: s1<s2 and
A2: t1<t2 and
A3: P = { p where p is Point of TOP-REAL 2:
p`1 = s1 & p`2 <= t2 & p`2 >= t1 or p`1 <= s2 & p`1 >= s1 & p`2 = t2 or
p`1 <= s2 & p`1 >= s1 & p`2 = t1 or p`1 = s2 & p`2 <= t2 & p`2 >= t1};
reconsider P1= {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2},
P2= {pc where pc is Point of TOP-REAL 2:
not( s1<=pc`1 & pc`1<=s2 & t1<=pc`2 & pc`2<=t2)}
as Subset of TOP-REAL 2 by Th23,Th24;
reconsider PC = P` as Subset of TOP-REAL 2;
A4: P1= {pa where pa is Point of TOP-REAL 2: s1<pa`1 & pa`1<s2 & t1 <pa`2 &
pa`2 < t2};
A5: P2= {pc where pc is Point of TOP-REAL 2: not( s1<=pc`1 & pc`1<=s2 & t1<=
pc`2 & pc`2<=t2)};
A6: PC=P1 \/ P2 by A1,A2,A3,Th30;
A7: PC<>{} by A1,A2,A3,A4,A5,Th30;
A8: P1 misses P2 by A1,A2,A3,Th30;
A9: P=(Cl P1)\P1 by A1,A2,A3,A5,Th31;
A10: P=(Cl P2)\P2 by A1,A2,A3,A4,Th31;
for P1A,P2B be Subset of (TOP-REAL 2)|P` holds P1A=P1 & P2B=P2 implies
P1A is a_component & P2B is a_component by A1,A2,A3,Th30;
hence thesis by A6,A7,A8,A9,A10;
end;
theorem
for s1,t1,s2,t2 for P,P2 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P2 = {pb where pb is Point of TOP-REAL 2:
not( s1<=pb`1 & pb`1<=s2 & t1<=pb`2 & pb`2<=t2)}
holds Cl P2 = P \/ P2 by Lm11;
theorem
for s1,t1,s2,t2 for P,P1 being Subset of TOP-REAL 2 st s1<s2 & t1<t2 &
P = { p where p is Point of TOP-REAL 2: p`1 = s1 & p`2 <= t2 & p`2 >= t1 or
p`1 <= s2 & p`1 >= s1 & p`2 = t2 or p`1 <= s2 & p`1 >= s1 & p`2 = t1 or
p`1 = s2 & p`2 <= t2 & p`2 >= t1} &
P1 = {pa where pa is Point of TOP-REAL 2:
s1<pa`1 & pa`1<s2 & t1 <pa`2 & pa`2 < t2} holds Cl P1 = P \/ P1 by Lm10;
:: Moved from JORDAN1H, AK, 22.02.2006
theorem
for p,q being Point of TOP-REAL 2 holds LSeg(p,q) \ {p,q} is convex
proof
let p,q,w1,w2 be Point of TOP-REAL 2;
set P = LSeg(p,q) \ {p,q};
assume that
A1: w1 in P and
A2: w2 in P;
A3: w1 in LSeg(p,q) by A1,XBOOLE_0:def 5;
A4: w2 in LSeg(p,q) by A2,XBOOLE_0:def 5;
A5: not w1 in {p,q} by A1,XBOOLE_0:def 5;
A6: not w2 in {p,q} by A2,XBOOLE_0:def 5;
A7: w1 <> p by A5,TARSKI:def 2;
A8: w2 <> p by A6,TARSKI:def 2;
A9: w1 <> q by A5,TARSKI:def 2;
A10: w2 <> q by A6,TARSKI:def 2;
A11: not p in LSeg(w1,w2) by A3,A4,A7,A8,SPPOL_1:7,TOPREAL1:6;
not q in LSeg(w1,w2) by A3,A4,A9,A10,SPPOL_1:7,TOPREAL1:6;
then LSeg(w1,w2) misses {p,q} by A11,ZFMISC_1:51;
hence thesis by A3,A4,TOPREAL1:6,XBOOLE_1:86;
end;
:: Moved from JORDAN1A, AK, 22.02.2006
Lm12: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x,y0 ]| where x is Real : x <= x0 } holds P is convex
proof
let x0,y0 be Real;
let P be Subset of TOP-REAL 2;
assume
A1: P = {|[ x,y0 ]| where x is Real : x <= x0 };
let w1,w2 be Point of TOP-REAL 2;
assume that
A2: w1 in P and
A3: w2 in P;
consider x1 being Real such that
A4: w1 = |[ x1,y0 ]| and
A5: x1 <= x0 by A1,A2;
consider x2 being Real such that
A6: w2 = |[ x2,y0 ]| and
A7: x2 <= x0 by A1,A3;
let v be object;
assume
A8: v in LSeg(w1,w2);
then reconsider v1 = v as Point of TOP-REAL 2;
consider l being Real such that
A9: v1 = (1-l)*w1 + l*w2 and
A10: 0 <= l and
A11: l <= 1 by A8;
A12: v1 = |[ (1-l)*x1,(1-l)*y0 ]| + l*|[ x2,y0 ]| by A4,A6,A9,EUCLID:58
.= |[ (1-l)*x1,(1-l)*y0 ]| + |[ l*x2,l*y0 ]| by EUCLID:58
.= |[ (1-l)*x1+l*x2,(1-l)*y0+l*y0 ]| by EUCLID:56
.= |[ (1-l)*x1+l*x2,1 * y0 ]|;
(1-l)*x1+l*x2 <= x0 by A5,A7,A10,A11,XREAL_1:174;
hence thesis by A1,A12;
end;
Lm13: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x0,y ]| where y is Real : y <= y0 } holds P is convex
proof
let x0,y0 be Real;
let P be Subset of TOP-REAL 2;
assume
A1: P = {|[ x0,y ]| where y is Real : y <= y0 };
let w1,w2 be Point of TOP-REAL 2;
assume that
A2: w1 in P and
A3: w2 in P;
consider y1 being Real such that
A4: w1 = |[ x0,y1 ]| and
A5: y1 <= y0 by A1,A2;
consider y2 being Real such that
A6: w2 = |[ x0,y2 ]| and
A7: y2 <= y0 by A1,A3;
let v be object;
assume
A8: v in LSeg(w1,w2);
then reconsider v1 = v as Point of TOP-REAL 2;
consider l being Real such that
A9: v1 = (1-l)*w1 + l*w2 and
A10: 0 <= l and
A11: l <= 1 by A8;
A12: v1 = |[ (1-l)*x0,(1-l)*y1 ]| + l*|[ x0,y2 ]| by A4,A6,A9,EUCLID:58
.= |[ (1-l)*x0,(1-l)*y1 ]| + |[ l*x0,l*y2 ]| by EUCLID:58
.= |[ (1-l)*x0+l*x0,(1-l)*y1+l*y2 ]| by EUCLID:56
.= |[ 1 * x0,(1-l)*y1+l*y2 ]|;
(1-l)*y1+l*y2 <= y0 by A5,A7,A10,A11,XREAL_1:174;
hence thesis by A1,A12;
end;
Lm14: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x,y0 ]| where x is Real : x >= x0 } holds P is convex
proof
let x0,y0 be Real;
let P be Subset of TOP-REAL 2;
assume
A1: P = {|[ x,y0 ]| where x is Real : x >= x0 };
let w1,w2 be Point of TOP-REAL 2;
assume that
A2: w1 in P and
A3: w2 in P;
consider x1 being Real such that
A4: w1 = |[ x1,y0 ]| and
A5: x1 >= x0 by A1,A2;
consider x2 being Real such that
A6: w2 = |[ x2,y0 ]| and
A7: x2 >= x0 by A1,A3;
let v be object;
assume
A8: v in LSeg(w1,w2);
then reconsider v1 = v as Point of TOP-REAL 2;
v1 in { (1-l)*w2 + l*w1 where l is Real : 0 <= l & l <= 1 }
by A8,RLTOPSP1:def 2;
then consider l being Real such that
A9: v1 = (1-l)*w2 + l*w1 and
A10: 0 <= l and
A11: l <= 1;
A12: v1 = |[ (1-l)*x2,(1-l)*y0 ]| + l*|[ x1,y0 ]| by A4,A6,A9,EUCLID:58
.= |[ (1-l)*x2,(1-l)*y0 ]| + |[ l*x1,l*y0 ]| by EUCLID:58
.= |[ (1-l)*x2+l*x1,(1-l)*y0+l*y0 ]| by EUCLID:56
.= |[ (1-l)*x2+l*x1,1 * y0 ]|;
(1-l)*x2+l*x1 >= x0 by A5,A7,A10,A11,XREAL_1:173;
hence thesis by A1,A12;
end;
Lm15: for x0,y0 being Real for P being Subset of TOP-REAL 2 st
P = {|[ x0,y ]| where y is Real : y >= y0 } holds P is convex
proof
let x0,y0 be Real;
let P be Subset of TOP-REAL 2;
assume
A1: P = {|[ x0,y ]| where y is Real : y >= y0 };
let w1,w2 be Point of TOP-REAL 2;
assume that
A2: w1 in P and
A3: w2 in P;
consider x1 being Real such that
A4: w1 = |[ x0,x1 ]| and
A5: x1 >= y0 by A1,A2;
consider x2 being Real such that
A6: w2 = |[ x0,x2 ]| and
A7: x2 >= y0 by A1,A3;
let v be object;
assume
A8: v in LSeg(w1,w2);
then reconsider v1 = v as Point of TOP-REAL 2;
v1 in { (1-l)*w2 + l*w1 where l is Real : 0 <= l & l <= 1 }
by A8,RLTOPSP1:def 2;
then consider l being Real such that
A9: v1 = (1-l)*w2 + l*w1 and
A10: 0 <= l and
A11: l <= 1;
A12: v1 = |[ (1-l)*x0,(1-l)*x2 ]| + l*|[ x0,x1 ]| by A4,A6,A9,EUCLID:58
.= |[ (1-l)*x0,(1-l)*x2 ]| + |[ l*x0,l*x1 ]| by EUCLID:58
.= |[ (1-l)*x0+l*x0,(1-l)*x2+l*x1 ]| by EUCLID:56
.= |[ 1 * x0,(1-l)*x2+l*x1]|;
(1-l)*x2+l*x1 >= y0 by A5,A7,A10,A11,XREAL_1:173;
hence thesis by A1,A12;
end;
registration
let p be Point of TOP-REAL 2;
cluster north_halfline p -> convex;
coherence
proof
north_halfline p =
{ |[ p`1,r ]| where r is Real: r >= p`2 } by TOPREAL1:31;
hence thesis by Lm15;
end;
cluster east_halfline p -> convex;
coherence
proof
east_halfline p =
{ |[ r,p`2 ]| where r is Real: r >= p`1 } by TOPREAL1:33;
hence thesis by Lm14;
end;
cluster south_halfline p -> convex;
coherence
proof
south_halfline p =
{ |[ p`1,r ]| where r is Real: r <= p`2 } by TOPREAL1:35;
hence thesis by Lm13;
end;
cluster west_halfline p -> convex;
coherence
proof
west_halfline p =
{ |[ r,p`2 ]| where r is Real: r <= p`1 } by TOPREAL1:37;
hence thesis by Lm12;
end;
end;