let n, m be Nat; :: thesis: for T1, T2 being non empty TopSpace
for A being convex non boundary compact Subset of (TOP-REAL n)
for B being convex non boundary compact Subset of (TOP-REAL m)
for C being convex non boundary compact Subset of (TOP-REAL (n + m))
for f being Function of T1,((TOP-REAL n) | A)
for g being Function of T2,((TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds
ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )
let T1, T2 be non empty TopSpace; :: thesis: for A being convex non boundary compact Subset of (TOP-REAL n)
for B being convex non boundary compact Subset of (TOP-REAL m)
for C being convex non boundary compact Subset of (TOP-REAL (n + m))
for f being Function of T1,((TOP-REAL n) | A)
for g being Function of T2,((TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds
ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
set nm = n + m;
set TRnm = TOP-REAL (n + m);
let A be convex non boundary compact Subset of (TOP-REAL n); :: thesis: for B being convex non boundary compact Subset of (TOP-REAL m)
for C being convex non boundary compact Subset of (TOP-REAL (n + m))
for f being Function of T1,((TOP-REAL n) | A)
for g being Function of T2,((TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds
ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )
let B be convex non boundary compact Subset of (TOP-REAL m); :: thesis: for C being convex non boundary compact Subset of (TOP-REAL (n + m))
for f being Function of T1,((TOP-REAL n) | A)
for g being Function of T2,((TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds
ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )
let C be convex non boundary compact Subset of (TOP-REAL (n + m)); :: thesis: for f being Function of T1,((TOP-REAL n) | A)
for g being Function of T2,((TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds
ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )
let f be Function of T1,((TOP-REAL n) | A); :: thesis: for g being Function of T2,((TOP-REAL m) | B) st f is being_homeomorphism & g is being_homeomorphism holds
ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )
let g be Function of T2,((TOP-REAL m) | B); :: thesis: ( f is being_homeomorphism & g is being_homeomorphism implies ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) ) )
assume that
A1: f is being_homeomorphism and
A2: g is being_homeomorphism ; :: thesis: ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | C) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff h . (t1,t2) in Int C ) ) )
set Rn = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1));
set Rm = ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1));
set Rnm = ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1));
consider gm being Function of ((TOP-REAL m) | B),((TOP-REAL m) | (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) such that
A3: gm is being_homeomorphism and
A4: gm .: (Fr B) = Fr (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) by BROUWER2:7;
A5: gm .: (Int B) misses gm .: (Fr B) by A3, TOPS_1:39, FUNCT_1:66;
A6: not B is empty ;
then reconsider gmg = gm * g as Function of T2,((TOP-REAL m) | (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) ;
A7: gmg is being_homeomorphism by A2, A3, A6, TOPS_2:57;
then A8: dom gmg = [#] T2 by TOPS_2:def 5;
reconsider Rn = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) as non empty Subset of (TOP-REAL n) ;
consider fn being Function of ((TOP-REAL n) | A),((TOP-REAL n) | Rn) such that
A9: fn is being_homeomorphism and
A10: fn .: (Fr A) = Fr Rn by BROUWER2:7;
A11: fn .: (Int A) misses fn .: (Fr A) by A9, TOPS_1:39, FUNCT_1:66;
A12: not A is empty ;
then reconsider fnf = fn * f as Function of T1,((TOP-REAL n) | Rn) ;
A13: fnf is being_homeomorphism by A1, A9, A12, TOPS_2:57;
then A14: dom fnf = [#] T1 by TOPS_2:def 5;
A15: [#] ((TOP-REAL m) | (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) = ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)) by PRE_TOPC:def 5;
A16: Int C = C \ (Fr C) by TOPS_1:40;
A17: [#] ((TOP-REAL (n + m)) | C) = C by PRE_TOPC:def 5;
A18: Int (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) = (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) \ (Fr (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) by TOPS_1:40;
set OHn = OpenHypercube ((0. (TOP-REAL n)),1);
set OHm = OpenHypercube ((0. (TOP-REAL m)),1);
set OHnm = OpenHypercube ((0. (TOP-REAL (n + m))),1);
consider H being Function of ((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))),((TOP-REAL (n + m)) | C) such that
A19: H is being_homeomorphism and
A20: H .: (Fr (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) = Fr C by BROUWER2:7;
A21: H .: (Int (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) misses H .: (Fr (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) by A19, TOPS_1:39, FUNCT_1:66;
A22: Int (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) = OpenHypercube ((0. (TOP-REAL m)),1) by Th11;
consider P being Function of [:T1,T2:],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) such that
A23: P is being_homeomorphism and
A24: for t1 being Point of T1
for t2 being Point of T2 holds
( ( fnf . t1 in OpenHypercube ((0. (TOP-REAL n)),1) & gmg . t2 in OpenHypercube ((0. (TOP-REAL m)),1) ) iff P . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) ) by A7, A13, Th16;
reconsider HP = H * P as Function of [:T1,T2:],((TOP-REAL (n + m)) | C) ;
take HP ; :: thesis: ( HP is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff HP . (t1,t2) in Int C ) ) )
not C is empty ;
hence HP is being_homeomorphism by A23, A19, TOPS_2:57; :: thesis: for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff HP . (t1,t2) in Int C )
then A25: dom HP = [#] [:T1,T2:] by TOPS_2:def 5;
A26: [#] ((TOP-REAL n) | Rn) = Rn by PRE_TOPC:def 5;
A27: Int Rn = Rn \ (Fr Rn) by TOPS_1:40;
let t1 be Point of T1; :: thesis: for t2 being Point of T2 holds
( ( f . t1 in Int A & g . t2 in Int B ) iff HP . (t1,t2) in Int C )
let t2 be Point of T2; :: thesis: ( ( f . t1 in Int A & g . t2 in Int B ) iff HP . (t1,t2) in Int C )
A28: P . [t1,t2] in dom H by A25, FUNCT_1:11;
A29: Int (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1))) = OpenHypercube ((0. (TOP-REAL (n + m))),1) by Th11;
A30: HP . [t1,t2] in rng HP by A25, FUNCT_1:def 3;
thus ( f . t1 in Int A & g . t2 in Int B implies HP . (t1,t2) in Int C ) :: thesis: ( HP . (t1,t2) in Int C implies ( f . t1 in Int A & g . t2 in Int B ) )
proof
A31: f . t1 in dom fn by A14, FUNCT_1:11;
assume that
A32: f . t1 in Int A and
A33: g . t2 in Int B ; :: thesis: HP . (t1,t2) in Int C
fnf . t1 = fn . (f . t1) by A14, FUNCT_1:12;
then fnf . t1 in fn .: (Int A) by A31, A32, FUNCT_1:def 6;
then not fnf . t1 in Fr Rn by A10, A11, XBOOLE_0:3;
then fnf . t1 in Rn \ (Fr Rn) by A26, XBOOLE_0:def 5;
then A34: fnf . t1 in OpenHypercube ((0. (TOP-REAL n)),1) by Th11, A27;
A35: g . t2 in dom gm by A8, FUNCT_1:11;
A36: P . [t1,t2] in dom H by A25, FUNCT_1:11;
A37: HP . [t1,t2] = H . (P . [t1,t2]) by A25, FUNCT_1:12;
gmg . t2 = gm . (g . t2) by A8, FUNCT_1:12;
then gmg . t2 in gm .: (Int B) by A35, A33, FUNCT_1:def 6;
then not gmg . t2 in Fr (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) by A4, A5, XBOOLE_0:3;
then gmg . t2 in (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) \ (Fr (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) by A15, XBOOLE_0:def 5;
then P . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) by A24, A34, A22, A18;
then HP . [t1,t2] in H .: (Int (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) by A37, A36, FUNCT_1:def 6, A29;
then not HP . [t1,t2] in Fr C by XBOOLE_0:3, A21, A20;
hence HP . (t1,t2) in Int C by A16, A30, A17, XBOOLE_0:def 5; :: thesis: verum
end;
assume HP . (t1,t2) in Int C ; :: thesis: ( f . t1 in Int A & g . t2 in Int B )
then A38: not HP . [t1,t2] in H .: (Fr (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) by XBOOLE_0:def 5, A16, A20;
A39: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;
A40: [#] ((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) = ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)) by PRE_TOPC:def 5;
A41: gmg . t2 = gm . (g . t2) by A8, FUNCT_1:12;
A42: Int (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1))) = (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1))) \ (Fr (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) by TOPS_1:40;
A43: f . t1 in dom fn by A14, FUNCT_1:11;
A44: HP . [t1,t2] = H . (P . [t1,t2]) by A25, FUNCT_1:12;
P . [t1,t2] in Int (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))
proof
assume not P . [t1,t2] in Int (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1))) ; :: thesis: contradiction
then P . [t1,t2] in Fr (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1))) by A40, A42, XBOOLE_0:def 5;
hence contradiction by A44, A28, FUNCT_1:def 6, A38; :: thesis: verum
end;
then A45: P . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) by Th11;
then gmg . t2 in (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) \ (Fr (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) by A24, A22, A18;
then A46: not gmg . t2 in Fr (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) by XBOOLE_0:def 5;
Int Rn = OpenHypercube ((0. (TOP-REAL n)),1) by Th11;
then fnf . t1 in Rn \ (Fr Rn) by A45, A24, A27;
then A47: not fnf . t1 in Fr Rn by XBOOLE_0:def 5;
A48: fnf . t1 = fn . (f . t1) by A14, FUNCT_1:12;
thus f . t1 in Int A :: thesis: g . t2 in Int B
proof
assume not f . t1 in Int A ; :: thesis: contradiction
then not f . t1 in A \ (Fr A) by TOPS_1:40;
then f . t1 in Fr A by A39, A43, XBOOLE_0:def 5;
hence contradiction by A48, A43, FUNCT_1:def 6, A47, A10; :: thesis: verum
end;
assume not g . t2 in Int B ; :: thesis: contradiction
then A49: not g . t2 in B \ (Fr B) by TOPS_1:40;
A50: g . t2 in dom gm by A8, FUNCT_1:11;
[#] ((TOP-REAL m) | B) = B by PRE_TOPC:def 5;
then g . t2 in Fr B by A49, A50, XBOOLE_0:def 5;
hence contradiction by A41, A50, FUNCT_1:def 6, A46, A4; :: thesis: verum