:: TOPREAL5 semantic presentation
begin
Lm1: for X, Y, Z being non empty TopSpace
for f being continuous Function of X,Y
for g being continuous Function of Y,Z holds g * f is continuous Function of X,Z
;
theorem Th1: :: TOPREAL5:1
for X being non empty TopSpace
for A, B1, B2 being Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 holds
not A is connected
proof
let X be non empty TopSpace; ::_thesis: for A, B1, B2 being Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 holds
not A is connected
let A, B1, B2 be Subset of X; ::_thesis: ( B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 implies not A is connected )
assume that
A1: ( B1 is open & B2 is open & B1 meets A ) and
A2: B2 meets A and
A3: A c= B1 \/ B2 and
A4: B1 misses B2 ; ::_thesis: not A is connected
reconsider C1 = B1 /\ A, C2 = B2 /\ A as Subset of X ;
A5: A = (B1 \/ B2) /\ A by A3, XBOOLE_1:28
.= C1 \/ C2 by XBOOLE_1:23 ;
A6: C2 <> {} by A2, XBOOLE_0:def_7;
A7: ( A is connected iff for P, Q being Subset of X st A = P \/ Q & P,Q are_separated & not P = {} X holds
Q = {} X ) by CONNSP_1:15;
A8: ( C1 c= B1 & C2 c= B2 ) by XBOOLE_1:17;
( B1,B2 are_separated & C1 <> {} ) by A1, A4, TSEP_1:37, XBOOLE_0:def_7;
hence not A is connected by A7, A5, A8, A6, CONNSP_1:7; ::_thesis: verum
end;
theorem Th2: :: TOPREAL5:2
for ra, rb being real number st ra <= rb holds
[#] (Closed-Interval-TSpace (ra,rb)) is connected
proof
let ra, rb be real number ; ::_thesis: ( ra <= rb implies [#] (Closed-Interval-TSpace (ra,rb)) is connected )
assume ra <= rb ; ::_thesis: [#] (Closed-Interval-TSpace (ra,rb)) is connected
then Closed-Interval-TSpace (ra,rb) is connected by TREAL_1:20;
hence [#] (Closed-Interval-TSpace (ra,rb)) is connected by CONNSP_1:27; ::_thesis: verum
end;
theorem Th3: :: TOPREAL5:3
for A being Subset of R^1
for a being real number st not a in A & ex b, d being real number st
( b in A & d in A & b < a & a < d ) holds
not A is connected
proof
let A be Subset of R^1; ::_thesis: for a being real number st not a in A & ex b, d being real number st
( b in A & d in A & b < a & a < d ) holds
not A is connected
let a be real number ; ::_thesis: ( not a in A & ex b, d being real number st
( b in A & d in A & b < a & a < d ) implies not A is connected )
assume that
A1: not a in A and
A2: ex b, d being real number st
( b in A & d in A & b < a & a < d ) ; ::_thesis: not A is connected
consider b, d being real number such that
A3: b in A and
A4: d in A and
A5: b < a and
A6: a < d by A2;
set B2 = { s where s is Element of REAL : s > a } ;
set B1 = { r where r is Element of REAL : r < a } ;
A7: A c= { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a } )
assume A8: x in A ; ::_thesis: x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a }
then reconsider r = x as Real by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6;
( r < a or a < r ) by A1, A8, XXREAL_0:1;
then ( r in { r where r is Element of REAL : r < a } or r in { s where s is Element of REAL : s > a } ) ;
hence x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a } by XBOOLE_0:def_3; ::_thesis: verum
end;
{ s where s is Element of REAL : s > a } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { s where s is Element of REAL : s > a } or x in REAL )
assume x in { s where s is Element of REAL : s > a } ; ::_thesis: x in REAL
then ex r being Element of REAL st
( r = x & r > a ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider C2 = { s where s is Element of REAL : s > a } as Subset of R^1 by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6;
{ r where r is Element of REAL : r < a } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Element of REAL : r < a } or x in REAL )
assume x in { r where r is Element of REAL : r < a } ; ::_thesis: x in REAL
then ex r being Element of REAL st
( r = x & r < a ) ;
hence x in REAL ; ::_thesis: verum
end;
then reconsider C1 = { r where r is Element of REAL : r < a } as Subset of R^1 by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6;
A9: now__::_thesis:_not__{__r_where_r_is_Element_of_REAL_:_r_<_a__}__meets__{__s_where_s_is_Element_of_REAL_:_s_>_a__}_
assume { r where r is Element of REAL : r < a } meets { s where s is Element of REAL : s > a } ; ::_thesis: contradiction
then consider x being set such that
A10: x in { r where r is Element of REAL : r < a } /\ { s where s is Element of REAL : s > a } by XBOOLE_0:4;
x in { s where s is Element of REAL : s > a } by A10, XBOOLE_0:def_4;
then A11: ex r2 being Element of REAL st
( r2 = x & r2 > a ) ;
x in { r where r is Element of REAL : r < a } by A10, XBOOLE_0:def_4;
then ex r1 being Element of REAL st
( r1 = x & r1 < a ) ;
hence contradiction by A11; ::_thesis: verum
end;
reconsider r1 = d as Element of REAL by XREAL_0:def_1;
r1 in { s where s is Element of REAL : s > a } by A6;
then d in { s where s is Element of REAL : s > a } /\ A by A4, XBOOLE_0:def_4;
then A12: { s where s is Element of REAL : s > a } meets A by XBOOLE_0:4;
reconsider r = b as Element of REAL by XREAL_0:def_1;
r in { r where r is Element of REAL : r < a } by A5;
then b in { r where r is Element of REAL : r < a } /\ A by A3, XBOOLE_0:def_4;
then A13: { r where r is Element of REAL : r < a } meets A by XBOOLE_0:4;
( C1 is open & C2 is open ) by JORDAN2B:24, JORDAN2B:25;
hence not A is connected by A9, A13, A12, A7, Th1; ::_thesis: verum
end;
theorem :: TOPREAL5:4
for X being non empty TopSpace
for xa, xb being Point of X
for a, b, d being Real
for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds
ex xc being Point of X st f . xc = d
proof
let X be non empty TopSpace; ::_thesis: for xa, xb being Point of X
for a, b, d being Real
for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds
ex xc being Point of X st f . xc = d
let xa, xb be Point of X; ::_thesis: for a, b, d being Real
for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds
ex xc being Point of X st f . xc = d
let a, b, d be Real; ::_thesis: for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds
ex xc being Point of X st f . xc = d
let f be continuous Function of X,R^1; ::_thesis: ( X is connected & f . xa = a & f . xb = b & a <= d & d <= b implies ex xc being Point of X st f . xc = d )
assume that
A1: X is connected and
A2: ( f . xa = a & f . xb = b ) and
A3: ( a <= d & d <= b ) ; ::_thesis: ex xc being Point of X st f . xc = d
now__::_thesis:_(_not_a_=_d_&_not_d_=_b_implies_ex_xc_being_Point_of_X_st_f_._xc_=_d_)
assume ( not a = d & not d = b ) ; ::_thesis: ex xc being Point of X st f . xc = d
then A4: ( a < d & d < b ) by A3, XXREAL_0:1;
now__::_thesis:_ex_rc_being_Point_of_X_st_f_._rc_=_d
assume A5: for rc being Point of X holds not f . rc = d ; ::_thesis: contradiction
A6: now__::_thesis:_not_d_in_f_.:_([#]_X)
assume d in f .: ([#] X) ; ::_thesis: contradiction
then ex x being set st
( x in the carrier of X & x in [#] X & d = f . x ) by FUNCT_2:64;
hence contradiction by A5; ::_thesis: verum
end;
dom f = the carrier of X by FUNCT_2:def_1;
then A7: ( a in f .: ([#] X) & b in f .: ([#] X) ) by A2, FUNCT_1:def_6;
[#] X is connected by A1, CONNSP_1:27;
hence contradiction by A4, A6, A7, Th3, TOPS_2:61; ::_thesis: verum
end;
hence ex xc being Point of X st f . xc = d ; ::_thesis: verum
end;
hence ex xc being Point of X st f . xc = d by A2; ::_thesis: verum
end;
theorem :: TOPREAL5:5
for X being non empty TopSpace
for xa, xb being Point of X
for B being Subset of X
for a, b, d being Real
for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds
ex xc being Point of X st
( xc in B & f . xc = d )
proof
let X be non empty TopSpace; ::_thesis: for xa, xb being Point of X
for B being Subset of X
for a, b, d being Real
for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds
ex xc being Point of X st
( xc in B & f . xc = d )
let xa, xb be Point of X; ::_thesis: for B being Subset of X
for a, b, d being Real
for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds
ex xc being Point of X st
( xc in B & f . xc = d )
let B be Subset of X; ::_thesis: for a, b, d being Real
for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds
ex xc being Point of X st
( xc in B & f . xc = d )
let a, b, d be Real; ::_thesis: for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds
ex xc being Point of X st
( xc in B & f . xc = d )
let f be continuous Function of X,R^1; ::_thesis: ( B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B implies ex xc being Point of X st
( xc in B & f . xc = d ) )
assume that
A1: B is connected and
A2: ( f . xa = a & f . xb = b ) and
A3: ( a <= d & d <= b ) and
A4: ( xa in B & xb in B ) ; ::_thesis: ex xc being Point of X st
( xc in B & f . xc = d )
now__::_thesis:_(_not_a_=_d_&_not_d_=_b_implies_ex_xc_being_Point_of_X_st_
(_xc_in_B_&_f_._xc_=_d_)_)
assume ( not a = d & not d = b ) ; ::_thesis: ex xc being Point of X st
( xc in B & f . xc = d )
then A5: ( a < d & d < b ) by A3, XXREAL_0:1;
now__::_thesis:_ex_rc_being_Point_of_X_st_
(_rc_in_B_&_f_._rc_=_d_)
assume A6: for rc being Point of X holds
( not rc in B or not f . rc = d ) ; ::_thesis: contradiction
A7: now__::_thesis:_not_d_in_f_.:_B
assume d in f .: B ; ::_thesis: contradiction
then ex x being set st
( x in the carrier of X & x in B & d = f . x ) by FUNCT_2:64;
hence contradiction by A6; ::_thesis: verum
end;
dom f = the carrier of X by FUNCT_2:def_1;
then ( a in f .: B & b in f .: B ) by A2, A4, FUNCT_1:def_6;
hence contradiction by A1, A5, A7, Th3, TOPS_2:61; ::_thesis: verum
end;
hence ex xc being Point of X st
( xc in B & f . xc = d ) ; ::_thesis: verum
end;
hence ex xc being Point of X st
( xc in B & f . xc = d ) by A2, A4; ::_thesis: verum
end;
theorem Th6: :: TOPREAL5:6
for ra, rb, a, b being real number st ra < rb holds
for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for d being real number st f . ra = a & f . rb = b & a < d & d < b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
proof
let ra, rb, a, b be real number ; ::_thesis: ( ra < rb implies for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for d being real number st f . ra = a & f . rb = b & a < d & d < b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) )
assume A1: ra < rb ; ::_thesis: for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for d being real number st f . ra = a & f . rb = b & a < d & d < b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
let f be continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1; ::_thesis: for d being real number st f . ra = a & f . rb = b & a < d & d < b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
let d be real number ; ::_thesis: ( f . ra = a & f . rb = b & a < d & d < b implies ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) )
assume that
A2: f . ra = a and
A3: f . rb = b and
A4: a < d and
A5: d < b ; ::_thesis: ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
now__::_thesis:_ex_rc_being_Element_of_REAL_st_
(_f_._rc_=_d_&_ra_<_rc_&_rc_<_rb_)
reconsider C = f .: ([#] (Closed-Interval-TSpace (ra,rb))) as Subset of R^1 ;
A6: dom f = the carrier of (Closed-Interval-TSpace (ra,rb)) by FUNCT_2:def_1;
A7: the carrier of (Closed-Interval-TSpace (ra,rb)) = [.ra,rb.] by A1, TOPMETR:18;
then rb in [#] (Closed-Interval-TSpace (ra,rb)) by A1, XXREAL_1:1;
then A8: b in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A3, A6, FUNCT_1:def_6;
assume A9: for rc being Element of REAL holds
( not f . rc = d or not ra < rc or not rc < rb ) ; ::_thesis: contradiction
A10: now__::_thesis:_not_d_in_f_.:_([#]_(Closed-Interval-TSpace_(ra,rb)))
assume d in f .: ([#] (Closed-Interval-TSpace (ra,rb))) ; ::_thesis: contradiction
then consider x being set such that
A11: x in the carrier of (Closed-Interval-TSpace (ra,rb)) and
x in [#] (Closed-Interval-TSpace (ra,rb)) and
A12: d = f . x by FUNCT_2:64;
reconsider r = x as Real by A7, A11;
r <= rb by A7, A11, XXREAL_1:1;
then A13: r < rb by A3, A5, A12, XXREAL_0:1;
ra <= r by A7, A11, XXREAL_1:1;
then ra < r by A2, A4, A12, XXREAL_0:1;
hence contradiction by A9, A12, A13; ::_thesis: verum
end;
ra in [#] (Closed-Interval-TSpace (ra,rb)) by A1, A7, XXREAL_1:1;
then a in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A2, A6, FUNCT_1:def_6;
then not C is connected by A4, A5, A10, A8, Th3;
hence contradiction by A1, Th2, TOPS_2:61; ::_thesis: verum
end;
hence ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) ; ::_thesis: verum
end;
theorem Th7: :: TOPREAL5:7
for ra, rb, a, b being real number st ra < rb holds
for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for d being real number st f . ra = a & f . rb = b & a > d & d > b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
proof
let ra, rb, a, b be real number ; ::_thesis: ( ra < rb implies for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for d being real number st f . ra = a & f . rb = b & a > d & d > b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) )
assume A1: ra < rb ; ::_thesis: for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for d being real number st f . ra = a & f . rb = b & a > d & d > b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
then A2: the carrier of (Closed-Interval-TSpace (ra,rb)) = [.ra,rb.] by TOPMETR:18;
let f be continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1; ::_thesis: for d being real number st f . ra = a & f . rb = b & a > d & d > b holds
ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
let d be real number ; ::_thesis: ( f . ra = a & f . rb = b & a > d & d > b implies ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) )
assume that
A3: f . ra = a and
A4: f . rb = b and
A5: a > d and
A6: d > b ; ::_thesis: ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb )
A7: dom f = the carrier of (Closed-Interval-TSpace (ra,rb)) by FUNCT_2:def_1;
A8: [#] (Closed-Interval-TSpace (ra,rb)) is connected by A1, Th2;
now__::_thesis:_ex_rc_being_Element_of_REAL_st_
(_ra_<_rc_&_rc_<_rb_&_not_f_._rc_<>_d_)
assume A9: for rc being Element of REAL st ra < rc & rc < rb holds
f . rc <> d ; ::_thesis: contradiction
A10: now__::_thesis:_not_d_in_f_.:_([#]_(Closed-Interval-TSpace_(ra,rb)))
assume d in f .: ([#] (Closed-Interval-TSpace (ra,rb))) ; ::_thesis: contradiction
then consider x being set such that
A11: x in dom f and
x in [#] (Closed-Interval-TSpace (ra,rb)) and
A12: d = f . x by FUNCT_1:def_6;
x in [.ra,rb.] by A2, A11;
then reconsider r = x as Real ;
r <= rb by A2, A11, XXREAL_1:1;
then A13: rb > r by A4, A6, A12, XXREAL_0:1;
ra <= r by A2, A11, XXREAL_1:1;
then ra < r by A3, A5, A12, XXREAL_0:1;
hence contradiction by A9, A12, A13; ::_thesis: verum
end;
rb in [.ra,rb.] by A1, XXREAL_1:1;
then A14: b in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A4, A2, A7, FUNCT_1:def_6;
ra in [.ra,rb.] by A1, XXREAL_1:1;
then a in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A3, A2, A7, FUNCT_1:def_6;
hence contradiction by A5, A6, A8, A10, A14, Th3, TOPS_2:61; ::_thesis: verum
end;
hence ex rc being Element of REAL st
( f . rc = d & ra < rc & rc < rb ) ; ::_thesis: verum
end;
theorem :: TOPREAL5:8
for ra, rb being real number
for g being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds
ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb )
proof
let ra, rb be real number ; ::_thesis: for g being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1
for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds
ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb )
let g be continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1; ::_thesis: for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds
ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb )
let s1, s2 be real number ; ::_thesis: ( ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb implies ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb ) )
assume that
A1: ra < rb and
A2: s1 * s2 < 0 ; ::_thesis: ( not s1 = g . ra or not s2 = g . rb or ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb ) )
( ( s1 > 0 & s2 < 0 ) or ( s1 < 0 & s2 > 0 ) ) by A2, XREAL_1:133;
hence ( not s1 = g . ra or not s2 = g . rb or ex r1 being Element of REAL st
( g . r1 = 0 & ra < r1 & r1 < rb ) ) by A1, Th6, Th7; ::_thesis: verum
end;
theorem Th9: :: TOPREAL5:9
for g being Function of I[01],R^1
for s1, s2 being real number st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds
ex r1 being Element of REAL st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )
proof
let g be Function of I[01],R^1; ::_thesis: for s1, s2 being real number st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds
ex r1 being Element of REAL st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )
let s1, s2 be real number ; ::_thesis: ( g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 implies ex r1 being Element of REAL st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) )
assume that
A1: g is continuous and
A2: g . 0 <> g . 1 and
A3: ( s1 = g . 0 & s2 = g . 1 ) ; ::_thesis: ex r1 being Element of REAL st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )
now__::_thesis:_(_(_s1_<_s2_&_ex_rc_being_Element_of_REAL_st_
(_g_._rc_=_(s1_+_s2)_/_2_&_0_<_rc_&_rc_<_1_)_)_or_(_s2_<_s1_&_ex_rc_being_Element_of_REAL_st_
(_g_._rc_=_(s1_+_s2)_/_2_&_0_<_rc_&_rc_<_1_)_)_)
percases ( s1 < s2 or s2 < s1 ) by A2, A3, XXREAL_0:1;
case s1 < s2 ; ::_thesis: ex rc being Element of REAL st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 )
then ( s1 < (s1 + s2) / 2 & (s1 + s2) / 2 < s2 ) by XREAL_1:226;
hence ex rc being Element of REAL st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) by A1, A3, Th6, TOPMETR:20; ::_thesis: verum
end;
case s2 < s1 ; ::_thesis: ex rc being Element of REAL st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 )
then ( s2 < (s1 + s2) / 2 & (s1 + s2) / 2 < s1 ) by XREAL_1:226;
hence ex rc being Element of REAL st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) by A1, A3, Th7, TOPMETR:20; ::_thesis: verum
end;
end;
end;
hence ex r1 being Element of REAL st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) ; ::_thesis: verum
end;
begin
theorem Th10: :: TOPREAL5:10
for f being Function of (TOP-REAL 2),R^1 st f = proj1 holds
f is continuous
proof
let f be Function of (TOP-REAL 2),R^1; ::_thesis: ( f = proj1 implies f is continuous )
assume f = proj1 ; ::_thesis: f is continuous
then ( 1 in Seg 2 & ( for p being Element of (TOP-REAL 2) holds f . p = p /. 1 ) ) by FINSEQ_1:1, JORDAN2B:30;
hence f is continuous by JORDAN2B:18; ::_thesis: verum
end;
theorem Th11: :: TOPREAL5:11
for f being Function of (TOP-REAL 2),R^1 st f = proj2 holds
f is continuous
proof
let f be Function of (TOP-REAL 2),R^1; ::_thesis: ( f = proj2 implies f is continuous )
assume f = proj2 ; ::_thesis: f is continuous
then ( 2 in Seg 2 & ( for p being Element of (TOP-REAL 2) holds f . p = p /. 2 ) ) by FINSEQ_1:1, JORDAN2B:30;
hence f is continuous by JORDAN2B:18; ::_thesis: verum
end;
theorem Th12: :: TOPREAL5:12
for P being non empty Subset of (TOP-REAL 2)
for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds
ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) )
proof
reconsider rj = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty Subset of (TOP-REAL 2); ::_thesis: for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds
ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) )
let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: ( f is continuous implies ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) ) )
assume A1: f is continuous ; ::_thesis: ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = g . r ) )
reconsider f1 = f as Function ;
set h = (proj1 | P) * f;
A2: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5;
then A3: rng f1 c= P by RELAT_1:def_19;
rj is continuous Function of (TOP-REAL 2),R^1 by Th10;
then rj | ((TOP-REAL 2) | P) is continuous Function of ((TOP-REAL 2) | P),R^1 ;
then rj | P is continuous Function of ((TOP-REAL 2) | P),R^1 by A2, TMAP_1:def_3;
then reconsider h2 = (proj1 | P) * f as continuous Function of I[01],R^1 by A1, Lm1;
take h2 ; ::_thesis: ( h2 is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = h2 . r ) )
thus h2 is continuous ; ::_thesis: for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = h2 . r
let r be Real; ::_thesis: for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `1 = h2 . r
let q be Point of (TOP-REAL 2); ::_thesis: ( r in the carrier of I[01] & q = f . r implies q `1 = h2 . r )
assume that
A4: r in the carrier of I[01] and
A5: q = f . r ; ::_thesis: q `1 = h2 . r
A6: dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1;
A7: r in dom f1 by A4, FUNCT_2:def_1;
then f1 . r in rng f1 by FUNCT_1:def_3;
then A8: q in (dom proj1) /\ P by A5, A3, A6, XBOOLE_0:def_4;
thus h2 . r = (proj1 | P) . q by A5, A7, FUNCT_1:13
.= proj1 . q by A8, FUNCT_1:48
.= q `1 by PSCOMP_1:def_5 ; ::_thesis: verum
end;
theorem Th13: :: TOPREAL5:13
for P being non empty Subset of (TOP-REAL 2)
for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds
ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `2 = g . r ) )
proof
reconsider rj = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty Subset of (TOP-REAL 2); ::_thesis: for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds
ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `2 = g . r ) )
let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: ( f is continuous implies ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `2 = g . r ) ) )
assume A1: f is continuous ; ::_thesis: ex g being Function of I[01],R^1 st
( g is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `2 = g . r ) )
reconsider f1 = f as Function ;
set h = (proj2 | P) * f;
A2: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5;
then A3: rng f1 c= P by RELAT_1:def_19;
rj is continuous by Th11;
then rj | ((TOP-REAL 2) | P) is continuous Function of ((TOP-REAL 2) | P),R^1 ;
then rj | P is continuous Function of ((TOP-REAL 2) | P),R^1 by A2, TMAP_1:def_3;
then reconsider h2 = (proj2 | P) * f as continuous Function of I[01],R^1 by A1, Lm1;
take h2 ; ::_thesis: ( h2 is continuous & ( for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `2 = h2 . r ) )
thus h2 is continuous ; ::_thesis: for r being Element of REAL
for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `2 = h2 . r
let r be Real; ::_thesis: for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds
q `2 = h2 . r
let q be Point of (TOP-REAL 2); ::_thesis: ( r in the carrier of I[01] & q = f . r implies q `2 = h2 . r )
assume that
A4: r in the carrier of I[01] and
A5: q = f . r ; ::_thesis: q `2 = h2 . r
A6: dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1;
A7: r in dom f1 by A4, FUNCT_2:def_1;
then f1 . r in rng f1 by FUNCT_1:def_3;
then A8: q in (dom proj2) /\ P by A5, A3, A6, XBOOLE_0:def_4;
thus h2 . r = (proj2 | P) . q by A5, A7, FUNCT_1:13
.= proj2 . q by A8, FUNCT_1:48
.= q `2 by PSCOMP_1:def_6 ; ::_thesis: verum
end;
theorem Th14: :: TOPREAL5:14
for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r )
proof
let P be non empty Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r ) )
assume A1: P is being_simple_closed_curve ; ::_thesis: for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r )
now__::_thesis:_for_r0_being_real_number_ex_p_being_Point_of_(TOP-REAL_2)_st_
(_p_in_P_&_not_p_`2_=_r0_)
A2: [.0,1.] = ].0,1.[ \/ {0,1} by XXREAL_1:128;
given r0 being real number such that A3: for p being Point of (TOP-REAL 2) st p in P holds
p `2 = r0 ; ::_thesis: contradiction
consider p1, p2 being Point of (TOP-REAL 2), P1, P2 being non empty Subset of (TOP-REAL 2) such that
A4: p1 <> p2 and
A5: p1 in P and
A6: p2 in P and
A7: P1 is_an_arc_of p1,p2 and
A8: P2 is_an_arc_of p1,p2 and
A9: P = P1 \/ P2 and
A10: P1 /\ P2 = {p1,p2} by A1, TOPREAL2:6;
A11: p1 `2 = r0 by A3, A5;
A12: p2 `2 = r0 by A3, A6;
then A13: p1 `2 = p2 `2 by A3, A5;
A14: now__::_thesis:_not_p1_`1_=_p2_`1
assume p1 `1 = p2 `1 ; ::_thesis: contradiction
then p1 = |[(p2 `1),(p2 `2)]| by A13, EUCLID:53;
hence contradiction by A4, EUCLID:53; ::_thesis: verum
end;
consider f2 being Function of I[01],((TOP-REAL 2) | P2) such that
A15: f2 is being_homeomorphism and
A16: f2 . 0 = p1 and
A17: f2 . 1 = p2 by A8, TOPREAL1:def_1;
f2 is continuous by A15, TOPS_2:def_5;
then consider g2 being Function of I[01],R^1 such that
A18: g2 is continuous and
A19: for r being Element of REAL
for q2 being Point of (TOP-REAL 2) st r in the carrier of I[01] & q2 = f2 . r holds
q2 `1 = g2 . r by Th12;
A20: [#] ((TOP-REAL 2) | P2) = P2 by PRE_TOPC:def_5;
1 in {0,1} by TARSKI:def_2;
then A21: 1 in the carrier of I[01] by A2, BORSUK_1:40, XBOOLE_0:def_3;
then A22: p2 `1 = g2 . 1 by A17, A19;
0 in {0,1} by TARSKI:def_2;
then A23: 0 in the carrier of I[01] by A2, BORSUK_1:40, XBOOLE_0:def_3;
then p1 `1 = g2 . 0 by A16, A19;
then consider r2 being Element of REAL such that
A24: ( 0 < r2 & r2 < 1 ) and
A25: g2 . r2 = ((p1 `1) + (p2 `1)) / 2 by A18, A22, A14, Th9;
A26: [.0,1.] = { r3 where r3 is Element of REAL : ( 0 <= r3 & r3 <= 1 ) } by RCOMP_1:def_1;
then A27: r2 in the carrier of I[01] by A24, BORSUK_1:40;
dom f2 = the carrier of I[01] by FUNCT_2:def_1;
then A28: f2 . r2 in rng f2 by A27, FUNCT_1:def_3;
then A29: f2 . r2 in P by A9, A20, XBOOLE_0:def_3;
f2 . r2 in P2 by A28, A20;
then reconsider p4 = f2 . r2 as Point of (TOP-REAL 2) ;
A30: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5;
consider f1 being Function of I[01],((TOP-REAL 2) | P1) such that
A31: f1 is being_homeomorphism and
A32: f1 . 0 = p1 and
A33: f1 . 1 = p2 by A7, TOPREAL1:def_1;
f1 is continuous by A31, TOPS_2:def_5;
then consider g1 being Function of I[01],R^1 such that
A34: g1 is continuous and
A35: for r being Element of REAL
for q1 being Point of (TOP-REAL 2) st r in the carrier of I[01] & q1 = f1 . r holds
q1 `1 = g1 . r by Th12;
A36: p2 `1 = g1 . 1 by A33, A35, A21;
p1 `1 = g1 . 0 by A32, A35, A23;
then consider r1 being Element of REAL such that
A37: ( 0 < r1 & r1 < 1 ) and
A38: g1 . r1 = ((p1 `1) + (p2 `1)) / 2 by A34, A36, A14, Th9;
A39: r1 in the carrier of I[01] by A37, A26, BORSUK_1:40;
then r1 in dom f1 by FUNCT_2:def_1;
then A40: f1 . r1 in rng f1 by FUNCT_1:def_3;
then f1 . r1 in P1 by A30;
then reconsider p3 = f1 . r1 as Point of (TOP-REAL 2) ;
f1 . r1 in P by A9, A40, A30, XBOOLE_0:def_3;
then A41: p3 `2 = r0 by A3
.= p4 `2 by A3, A29 ;
p3 `1 = ((p1 `1) + (p2 `1)) / 2 by A35, A38, A39
.= p4 `1 by A19, A25, A27 ;
then f1 . r1 = f2 . r2 by A41, TOPREAL3:6;
then A42: f1 . r1 in P1 /\ P2 by A40, A30, A28, A20, XBOOLE_0:def_4;
now__::_thesis:_(_(_f1_._r1_=_p1_&_contradiction_)_or_(_f1_._r1_=_p2_&_contradiction_)_)
percases ( f1 . r1 = p1 or f1 . r1 = p2 ) by A10, A42, TARSKI:def_2;
caseA43: f1 . r1 = p1 ; ::_thesis: contradiction
A44: (((1 / 2) * p1) + ((1 / 2) * p2)) `2 = (((1 / 2) * p1) `2) + (((1 / 2) * p2) `2) by TOPREAL3:2
.= ((1 / 2) * (p1 `2)) + (((1 / 2) * p2) `2) by TOPREAL3:4
.= ((1 / 2) * r0) + ((1 / 2) * r0) by A11, A12, TOPREAL3:4
.= r0 ;
p1 `1 = ((2 ") * (p1 `1)) + ((p2 `1) / 2) by A35, A38, A39, A43
.= (((2 ") * p1) `1) + ((2 ") * (p2 `1)) by TOPREAL3:4
.= (((2 ") * p1) `1) + (((2 ") * p2) `1) by TOPREAL3:4
.= (((1 / 2) * p1) + ((1 / 2) * p2)) `1 by TOPREAL3:2 ;
then p1 = ((1 / 2) * p1) + ((1 / 2) * p2) by A11, A44, TOPREAL3:6;
then (1 * p1) - ((1 / 2) * p1) = (((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p1) by EUCLID:29;
then (1 * p1) - ((1 / 2) * p1) = ((1 / 2) * p2) + (((1 / 2) * p1) - ((1 / 2) * p1)) by EUCLID:45;
then (1 * p1) - ((1 / 2) * p1) = ((1 / 2) * p2) + (0. (TOP-REAL 2)) by EUCLID:42;
then (1 * p1) - ((1 / 2) * p1) = (1 / 2) * p2 by EUCLID:27;
then (1 - (1 / 2)) * p1 = (1 / 2) * p2 by EUCLID:50;
hence contradiction by A4, EUCLID:34; ::_thesis: verum
end;
caseA45: f1 . r1 = p2 ; ::_thesis: contradiction
A46: (((1 / 2) * p1) + ((1 / 2) * p2)) `2 = (((1 / 2) * p1) `2) + (((1 / 2) * p2) `2) by TOPREAL3:2
.= ((1 / 2) * (p1 `2)) + (((1 / 2) * p2) `2) by TOPREAL3:4
.= ((1 / 2) * r0) + ((1 / 2) * r0) by A11, A12, TOPREAL3:4
.= r0 ;
p2 `1 = ((2 ") * (p1 `1)) + ((p2 `1) / 2) by A35, A38, A39, A45
.= (((2 ") * p1) `1) + ((2 ") * (p2 `1)) by TOPREAL3:4
.= (((2 ") * p1) `1) + (((2 ") * p2) `1) by TOPREAL3:4
.= (((1 / 2) * p1) + ((1 / 2) * p2)) `1 by TOPREAL3:2 ;
then p2 = ((1 / 2) * p1) + ((1 / 2) * p2) by A12, A46, TOPREAL3:6;
then (1 * p2) - ((1 / 2) * p2) = (((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p2) by EUCLID:29;
then (1 * p2) - ((1 / 2) * p2) = ((1 / 2) * p1) + (((1 / 2) * p2) - ((1 / 2) * p2)) by EUCLID:45;
then (1 * p2) - ((1 / 2) * p2) = ((1 / 2) * p1) + (0. (TOP-REAL 2)) by EUCLID:42;
then (1 * p2) - ((1 / 2) * p2) = (1 / 2) * p1 by EUCLID:27;
then (1 - (1 / 2)) * p2 = (1 / 2) * p1 by EUCLID:50;
hence contradiction by A4, EUCLID:34; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `2 = r ) ; ::_thesis: verum
end;
theorem Th15: :: TOPREAL5:15
for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `1 = r )
proof
let P be non empty Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `1 = r ) )
assume A1: P is being_simple_closed_curve ; ::_thesis: for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `1 = r )
now__::_thesis:_for_r0_being_real_number_ex_p_being_Point_of_(TOP-REAL_2)_st_
(_p_in_P_&_not_p_`1_=_r0_)
A2: [.0,1.] = ].0,1.[ \/ {0,1} by XXREAL_1:128;
given r0 being real number such that A3: for p being Point of (TOP-REAL 2) st p in P holds
p `1 = r0 ; ::_thesis: contradiction
consider p1, p2 being Point of (TOP-REAL 2), P1, P2 being non empty Subset of (TOP-REAL 2) such that
A4: p1 <> p2 and
A5: p1 in P and
A6: p2 in P and
A7: P1 is_an_arc_of p1,p2 and
A8: P2 is_an_arc_of p1,p2 and
A9: P = P1 \/ P2 and
A10: P1 /\ P2 = {p1,p2} by A1, TOPREAL2:6;
A11: p1 `1 = r0 by A3, A5;
A12: p2 `1 = r0 by A3, A6;
then A13: p1 `1 = p2 `1 by A3, A5;
A14: now__::_thesis:_not_p1_`2_=_p2_`2
assume p1 `2 = p2 `2 ; ::_thesis: contradiction
then p1 = |[(p2 `1),(p2 `2)]| by A13, EUCLID:53;
hence contradiction by A4, EUCLID:53; ::_thesis: verum
end;
consider f2 being Function of I[01],((TOP-REAL 2) | P2) such that
A15: f2 is being_homeomorphism and
A16: f2 . 0 = p1 and
A17: f2 . 1 = p2 by A8, TOPREAL1:def_1;
f2 is continuous by A15, TOPS_2:def_5;
then consider g2 being Function of I[01],R^1 such that
A18: g2 is continuous and
A19: for r being Element of REAL
for q2 being Point of (TOP-REAL 2) st r in the carrier of I[01] & q2 = f2 . r holds
q2 `2 = g2 . r by Th13;
A20: [#] ((TOP-REAL 2) | P2) = P2 by PRE_TOPC:def_5;
1 in {0,1} by TARSKI:def_2;
then A21: 1 in the carrier of I[01] by A2, BORSUK_1:40, XBOOLE_0:def_3;
then A22: p2 `2 = g2 . 1 by A17, A19;
0 in {0,1} by TARSKI:def_2;
then A23: 0 in the carrier of I[01] by A2, BORSUK_1:40, XBOOLE_0:def_3;
then p1 `2 = g2 . 0 by A16, A19;
then consider r2 being Element of REAL such that
A24: ( 0 < r2 & r2 < 1 ) and
A25: g2 . r2 = ((p1 `2) + (p2 `2)) / 2 by A18, A22, A14, Th9;
A26: [.0,1.] = { r3 where r3 is Element of REAL : ( 0 <= r3 & r3 <= 1 ) } by RCOMP_1:def_1;
then A27: r2 in the carrier of I[01] by A24, BORSUK_1:40;
dom f2 = the carrier of I[01] by FUNCT_2:def_1;
then A28: f2 . r2 in rng f2 by A27, FUNCT_1:def_3;
then A29: f2 . r2 in P by A9, A20, XBOOLE_0:def_3;
f2 . r2 in P2 by A28, A20;
then reconsider p4 = f2 . r2 as Point of (TOP-REAL 2) ;
A30: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5;
consider f1 being Function of I[01],((TOP-REAL 2) | P1) such that
A31: f1 is being_homeomorphism and
A32: f1 . 0 = p1 and
A33: f1 . 1 = p2 by A7, TOPREAL1:def_1;
f1 is continuous by A31, TOPS_2:def_5;
then consider g1 being Function of I[01],R^1 such that
A34: g1 is continuous and
A35: for r being Element of REAL
for q1 being Point of (TOP-REAL 2) st r in the carrier of I[01] & q1 = f1 . r holds
q1 `2 = g1 . r by Th13;
A36: p2 `2 = g1 . 1 by A33, A35, A21;
p1 `2 = g1 . 0 by A32, A35, A23;
then consider r1 being Element of REAL such that
A37: ( 0 < r1 & r1 < 1 ) and
A38: g1 . r1 = ((p1 `2) + (p2 `2)) / 2 by A34, A36, A14, Th9;
A39: r1 in the carrier of I[01] by A37, A26, BORSUK_1:40;
then r1 in dom f1 by FUNCT_2:def_1;
then A40: f1 . r1 in rng f1 by FUNCT_1:def_3;
then f1 . r1 in P1 by A30;
then reconsider p3 = f1 . r1 as Point of (TOP-REAL 2) ;
f1 . r1 in P by A9, A40, A30, XBOOLE_0:def_3;
then A41: p3 `1 = r0 by A3
.= p4 `1 by A3, A29 ;
p3 `2 = ((p1 `2) + (p2 `2)) / 2 by A35, A38, A39
.= p4 `2 by A19, A25, A27 ;
then f1 . r1 = f2 . r2 by A41, TOPREAL3:6;
then A42: f1 . r1 in P1 /\ P2 by A40, A30, A28, A20, XBOOLE_0:def_4;
now__::_thesis:_(_(_f1_._r1_=_p1_&_contradiction_)_or_(_f1_._r1_=_p2_&_contradiction_)_)
percases ( f1 . r1 = p1 or f1 . r1 = p2 ) by A10, A42, TARSKI:def_2;
caseA43: f1 . r1 = p1 ; ::_thesis: contradiction
A44: (((1 / 2) * p1) + ((1 / 2) * p2)) `1 = (((1 / 2) * p1) `1) + (((1 / 2) * p2) `1) by TOPREAL3:2
.= ((1 / 2) * (p1 `1)) + (((1 / 2) * p2) `1) by TOPREAL3:4
.= ((1 / 2) * r0) + ((1 / 2) * r0) by A11, A12, TOPREAL3:4
.= r0 ;
p1 `2 = ((2 ") * (p1 `2)) + ((p2 `2) / 2) by A35, A38, A39, A43
.= (((2 ") * p1) `2) + ((2 ") * (p2 `2)) by TOPREAL3:4
.= (((2 ") * p1) `2) + (((2 ") * p2) `2) by TOPREAL3:4
.= (((1 / 2) * p1) + ((1 / 2) * p2)) `2 by TOPREAL3:2 ;
then p1 = ((1 / 2) * p1) + ((1 / 2) * p2) by A11, A44, TOPREAL3:6;
then (1 * p1) - ((1 / 2) * p1) = (((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p1) by EUCLID:29;
then (1 * p1) - ((1 / 2) * p1) = ((1 / 2) * p2) + (((1 / 2) * p1) - ((1 / 2) * p1)) by EUCLID:45;
then (1 * p1) - ((1 / 2) * p1) = ((1 / 2) * p2) + (0. (TOP-REAL 2)) by EUCLID:42;
then (1 * p1) - ((1 / 2) * p1) = (1 / 2) * p2 by EUCLID:27;
then (1 - (1 / 2)) * p1 = (1 / 2) * p2 by EUCLID:50;
hence contradiction by A4, EUCLID:34; ::_thesis: verum
end;
caseA45: f1 . r1 = p2 ; ::_thesis: contradiction
A46: (((1 / 2) * p1) + ((1 / 2) * p2)) `1 = (((1 / 2) * p1) `1) + (((1 / 2) * p2) `1) by TOPREAL3:2
.= ((1 / 2) * (p1 `1)) + (((1 / 2) * p2) `1) by TOPREAL3:4
.= ((1 / 2) * r0) + ((1 / 2) * r0) by A11, A12, TOPREAL3:4
.= r0 ;
p2 `2 = ((2 ") * (p1 `2)) + ((p2 `2) / 2) by A35, A38, A39, A45
.= (((2 ") * p1) `2) + ((2 ") * (p2 `2)) by TOPREAL3:4
.= (((2 ") * p1) `2) + (((2 ") * p2) `2) by TOPREAL3:4
.= (((1 / 2) * p1) + ((1 / 2) * p2)) `2 by TOPREAL3:2 ;
then p2 = ((1 / 2) * p1) + ((1 / 2) * p2) by A12, A46, TOPREAL3:6;
then (1 * p2) - ((1 / 2) * p2) = (((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p2) by EUCLID:29;
then (1 * p2) - ((1 / 2) * p2) = ((1 / 2) * p1) + (((1 / 2) * p2) - ((1 / 2) * p2)) by EUCLID:45;
then (1 * p2) - ((1 / 2) * p2) = ((1 / 2) * p1) + (0. (TOP-REAL 2)) by EUCLID:42;
then (1 * p2) - ((1 / 2) * p2) = (1 / 2) * p1 by EUCLID:27;
then (1 - (1 / 2)) * p2 = (1 / 2) * p1 by EUCLID:50;
hence contradiction by A4, EUCLID:34; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence for r being Element of REAL ex p being Point of (TOP-REAL 2) st
( p in P & not p `1 = r ) ; ::_thesis: verum
end;
theorem Th16: :: TOPREAL5:16
for C being non empty compact Subset of (TOP-REAL 2) st C is being_simple_closed_curve holds
N-bound C > S-bound C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( C is being_simple_closed_curve implies N-bound C > S-bound C )
assume A1: C is being_simple_closed_curve ; ::_thesis: N-bound C > S-bound C
now__::_thesis:_not_N-bound_C_<=_S-bound_C
assume A2: N-bound C <= S-bound C ; ::_thesis: contradiction
for p being Point of (TOP-REAL 2) st p in C holds
p `2 = S-bound C
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p in C implies p `2 = S-bound C )
assume p in C ; ::_thesis: p `2 = S-bound C
then A3: ( S-bound C <= p `2 & p `2 <= N-bound C ) by PSCOMP_1:24;
then S-bound C <= N-bound C by XXREAL_0:2;
then S-bound C = N-bound C by A2, XXREAL_0:1;
hence p `2 = S-bound C by A3, XXREAL_0:1; ::_thesis: verum
end;
hence contradiction by A1, Th14; ::_thesis: verum
end;
hence N-bound C > S-bound C ; ::_thesis: verum
end;
theorem Th17: :: TOPREAL5:17
for C being non empty compact Subset of (TOP-REAL 2) st C is being_simple_closed_curve holds
E-bound C > W-bound C
proof
let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( C is being_simple_closed_curve implies E-bound C > W-bound C )
assume A1: C is being_simple_closed_curve ; ::_thesis: E-bound C > W-bound C
now__::_thesis:_not_E-bound_C_<=_W-bound_C
assume A2: E-bound C <= W-bound C ; ::_thesis: contradiction
for p being Point of (TOP-REAL 2) st p in C holds
p `1 = W-bound C
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p in C implies p `1 = W-bound C )
assume p in C ; ::_thesis: p `1 = W-bound C
then A3: ( W-bound C <= p `1 & p `1 <= E-bound C ) by PSCOMP_1:24;
then W-bound C <= E-bound C by XXREAL_0:2;
then W-bound C = E-bound C by A2, XXREAL_0:1;
hence p `1 = W-bound C by A3, XXREAL_0:1; ::_thesis: verum
end;
hence contradiction by A1, Th15; ::_thesis: verum
end;
hence E-bound C > W-bound C ; ::_thesis: verum
end;
theorem :: TOPREAL5:18
for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
S-min P <> N-max P
proof
let P be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies S-min P <> N-max P )
assume A1: P is being_simple_closed_curve ; ::_thesis: S-min P <> N-max P
now__::_thesis:_not_S-min_P_=_N-max_P
A2: ( |[(lower_bound (proj1 | (S-most P))),(S-bound P)]| = S-min P & |[(upper_bound (proj1 | (N-most P))),(N-bound P)]| = N-max P ) by PSCOMP_1:def_22, PSCOMP_1:def_26;
assume S-min P = N-max P ; ::_thesis: contradiction
then S-bound P = N-bound P by A2, SPPOL_2:1;
hence contradiction by A1, Th16; ::_thesis: verum
end;
hence S-min P <> N-max P ; ::_thesis: verum
end;
theorem :: TOPREAL5:19
for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds
W-min P <> E-max P
proof
let P be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies W-min P <> E-max P )
assume A1: P is being_simple_closed_curve ; ::_thesis: W-min P <> E-max P
now__::_thesis:_not_W-min_P_=_E-max_P
A2: ( |[(W-bound P),(lower_bound (proj2 | (W-most P)))]| = W-min P & |[(E-bound P),(upper_bound (proj2 | (E-most P)))]| = E-max P ) by PSCOMP_1:def_19, PSCOMP_1:def_23;
assume W-min P = E-max P ; ::_thesis: contradiction
then W-bound P = E-bound P by A2, SPPOL_2:1;
hence contradiction by A1, Th17; ::_thesis: verum
end;
hence W-min P <> E-max P ; ::_thesis: verum
end;
registration
cluster being_simple_closed_curve -> non horizontal non vertical for Element of K6( the carrier of (TOP-REAL 2));
coherence
for b1 being Simple_closed_curve holds
( not b1 is vertical & not b1 is horizontal )
proof
let S be Simple_closed_curve; ::_thesis: ( not S is vertical & not S is horizontal )
consider p1 being set such that
A1: p1 in S by XBOOLE_0:def_1;
reconsider p1 = p1 as Point of (TOP-REAL 2) by A1;
ex p2 being Point of (TOP-REAL 2) st
( p2 in S & p2 `1 <> p1 `1 ) by Th15;
hence not S is vertical by A1, SPPOL_1:def_3; ::_thesis: not S is horizontal
ex p2 being Point of (TOP-REAL 2) st
( p2 in S & p2 `2 <> p1 `2 ) by Th14;
hence not S is horizontal by A1, SPPOL_1:def_2; ::_thesis: verum
end;
end;