let p1, p2, p3, p4 be Point of (TOP-REAL 2); ( p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1) implies for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) holds
rng f meets rng g )
set K = rectangle ((- 1),1,(- 1),1);
set K0 = closed_inside_of_rectangle ((- 1),1,(- 1),1);
assume A1:
p1,p2,p3,p4 are_in_this_order_on rectangle ((- 1),1,(- 1),1)
; for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) holds
rng f meets rng g
reconsider j = 1 as non negative Real ;
reconsider P = circle (0,0,j) as non empty compact Subset of (TOP-REAL 2) ;
A2:
P = { p6 where p6 is Point of (TOP-REAL 2) : |.p6.| = 1 }
by Th24;
thus
for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) holds
rng f meets rng g
verumproof
let f,
g be
Function of
I[01],
(TOP-REAL 2);
( f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) implies rng f meets rng g )
assume that A3:
(
f is
continuous &
f is
one-to-one )
and A4:
(
g is
continuous &
g is
one-to-one )
and A5:
f . 0 = p1
and A6:
f . 1
= p3
and A7:
g . 0 = p2
and A8:
g . 1
= p4
and A9:
rng f c= closed_inside_of_rectangle (
(- 1),1,
(- 1),1)
and A10:
rng g c= closed_inside_of_rectangle (
(- 1),1,
(- 1),1)
;
rng f meets rng g
reconsider s =
Sq_Circ as
Function of
(TOP-REAL 2),
(TOP-REAL 2) ;
A11:
dom s = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 1;
reconsider f1 =
s * f as
Function of
I[01],
(TOP-REAL 2) ;
reconsider g1 =
s * g as
Function of
I[01],
(TOP-REAL 2) ;
s is
being_homeomorphism
by JGRAPH_3:43;
then A12:
s is
continuous
by TOPS_2:def 5;
A13:
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then
0 in dom f
by XXREAL_1:1;
then A14:
f1 . 0 = Sq_Circ . p1
by A5, FUNCT_1:13;
1
in dom f
by A13, XXREAL_1:1;
then A15:
f1 . 1
= Sq_Circ . p3
by A6, FUNCT_1:13;
A16:
dom g = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then
0 in dom g
by XXREAL_1:1;
then A17:
g1 . 0 = Sq_Circ . p2
by A7, FUNCT_1:13;
1
in dom g
by A16, XXREAL_1:1;
then A18:
g1 . 1
= Sq_Circ . p4
by A8, FUNCT_1:13;
defpred S1[
Point of
(TOP-REAL 2)]
means |.$1.| <= 1;
{ p8 where p8 is Point of (TOP-REAL 2) : S1[p8] } is
Subset of
(TOP-REAL 2)
from DOMAIN_1:sch 7();
then reconsider C0 =
{ p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } as
Subset of
(TOP-REAL 2) ;
A19:
s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1)) = C0
by Th27;
A20:
rng f1 c= C0
proof
let y be
object ;
TARSKI:def 3 ( not y in rng f1 or y in C0 )
assume
y in rng f1
;
y in C0
then consider x being
object such that A21:
x in dom f1
and A22:
y = f1 . x
by FUNCT_1:def 3;
A23:
x in dom f
by A21, FUNCT_1:11;
A24:
f . x in dom s
by A21, FUNCT_1:11;
f . x in rng f
by A23, FUNCT_1:3;
then
s . (f . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1))
by A9, A24, FUNCT_1:def 6;
hence
y in C0
by A19, A21, A22, FUNCT_1:12;
verum
end;
A25:
rng g1 c= C0
proof
let y be
object ;
TARSKI:def 3 ( not y in rng g1 or y in C0 )
assume
y in rng g1
;
y in C0
then consider x being
object such that A26:
x in dom g1
and A27:
y = g1 . x
by FUNCT_1:def 3;
A28:
x in dom g
by A26, FUNCT_1:11;
A29:
g . x in dom s
by A26, FUNCT_1:11;
g . x in rng g
by A28, FUNCT_1:3;
then
s . (g . x) in s .: (closed_inside_of_rectangle ((- 1),1,(- 1),1))
by A10, A29, FUNCT_1:def 6;
hence
y in C0
by A19, A26, A27, FUNCT_1:12;
verum
end;
reconsider q1 =
s . p1,
q2 =
s . p2,
q3 =
s . p3,
q4 =
s . p4 as
Point of
(TOP-REAL 2) ;
q1,
q2,
q3,
q4 are_in_this_order_on P
by A1, Th78;
then
rng f1 meets rng g1
by A2, A3, A4, A12, A14, A15, A17, A18, A20, A25, Th18;
then consider y being
object such that A30:
y in rng f1
and A31:
y in rng g1
by XBOOLE_0:3;
consider x1 being
object such that A32:
x1 in dom f1
and A33:
y = f1 . x1
by A30, FUNCT_1:def 3;
consider x2 being
object such that A34:
x2 in dom g1
and A35:
y = g1 . x2
by A31, FUNCT_1:def 3;
dom f1 c= dom f
by RELAT_1:25;
then A36:
f . x1 in rng f
by A32, FUNCT_1:3;
dom g1 c= dom g
by RELAT_1:25;
then A37:
g . x2 in rng g
by A34, FUNCT_1:3;
y = Sq_Circ . (f . x1)
by A32, A33, FUNCT_1:12;
then A38:
(Sq_Circ ") . y = f . x1
by A11, A36, FUNCT_1:32;
x1 in dom f
by A32, FUNCT_1:11;
then A39:
f . x1 in rng f
by FUNCT_1:def 3;
y = Sq_Circ . (g . x2)
by A34, A35, FUNCT_1:12;
then A40:
(Sq_Circ ") . y = g . x2
by A11, A37, FUNCT_1:32;
x2 in dom g
by A34, FUNCT_1:11;
then
g . x2 in rng g
by FUNCT_1:def 3;
hence
rng f meets rng g
by A38, A39, A40, XBOOLE_0:3;
verum
end;