let N, M be non empty locally_euclidean TopSpace; :: thesis: Int [:N,M:] = [:(Int N),(Int M):]
set NM = [:N,M:];
set IN = Int N;
set IM = Int M;
thus Int [:N,M:] c= [:(Int N),(Int M):] :: according to XBOOLE_0:def 10 :: thesis: [:(Int N),(Int M):] c= Int [:N,M:]
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Int [:N,M:] or z in [:(Int N),(Int M):] )
assume A1: z in Int [:N,M:] ; :: thesis: z in [:(Int N),(Int M):]
then reconsider p = z as Point of [:N,M:] ;
z in the carrier of [:N,M:] by A1;
then z in [: the carrier of N, the carrier of M:] by BORSUK_1:def 2;
then consider x, y being object such that
A2: x in the carrier of N and
A3: y in the carrier of M and
A4: z = [x,y] by ZFMISC_1:def 2;
reconsider y = y as Point of M by A3;
reconsider x = x as Point of N by A2;
assume A5: not z in [:(Int N),(Int M):] ; :: thesis: contradiction
per cases ( not x in Int N or not y in Int M ) by A5, A4, ZFMISC_1:87;
suppose A6: not x in Int N ; :: thesis: contradiction
consider W being a_neighborhood of y, m being Nat such that
A7: M | W, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by Def2;
x in ([#] N) \ (Int N) by A6, XBOOLE_0:def 5;
then x in Fr N by SUBSET_1:def 4;
then consider U being a_neighborhood of x, n being Nat, h being Function of (N | U),(Tdisk ((0. (TOP-REAL n)),1)) such that
A8: h is being_homeomorphism and
A9: h . x in Sphere ((0. (TOP-REAL n)),1) by Th5;
A10: y in Int W by CONNSP_2:def 1;
reconsider mn = m + n as Nat ;
set TRm = TOP-REAL m;
set TRn = TOP-REAL n;
set TRnm = TOP-REAL mn;
consider f being Function of (M | W),(Tdisk ((0. (TOP-REAL m)),1)) such that
A11: f is being_homeomorphism by A7, T_0TOPSP:def 1;
A12: not h . x in Ball ((0. (TOP-REAL n)),1) by TOPREAL9:19, A9, XBOOLE_0:3;
consider hf being Function of [:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):],(Tdisk ((0. (TOP-REAL mn)),1)) such that
A13: hf is being_homeomorphism and
A14: hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] = Ball ((0. (TOP-REAL mn)),1) by TIETZE_2:19;
set H = hf * [:h,f:];
[:h,f:] is being_homeomorphism by A8, A11, TIETZE_2:15;
then A15: hf * [:h,f:] is being_homeomorphism by A13, TOPS_2:57;
then A16: rng (hf * [:h,f:]) = [#] (Tdisk ((0. (TOP-REAL mn)),1)) by TOPS_2:def 5;
A17: Int W c= W by TOPS_1:16;
A18: Int U c= U by TOPS_1:16;
x in Int U by CONNSP_2:def 1;
then A19: [x,y] in [:U,W:] by A18, A17, A10, ZFMISC_1:87;
n + m in NAT by ORDINAL1:def 12;
then A20: [#] (Tdisk ((0. (TOP-REAL mn)),1)) = cl_Ball ((0. (TOP-REAL mn)),1) by BROUWER:3;
A21: [:(N | U),(M | W):] = [:N,M:] | [:U,W:] by BORSUK_3:22;
then dom (hf * [:h,f:]) = [#] ([:N,M:] | [:U,W:]) by A15, TOPS_2:def 5;
then A22: p in dom (hf * [:h,f:]) by A19, A4, PRE_TOPC:def 5;
then A23: [:h,f:] . p in dom hf by FUNCT_1:11;
dom [:h,f:] = [:(dom h),(dom f):] by FUNCT_3:def 8;
then A24: [:h,f:] . (x,y) = [(h . x),(f . y)] by A22, FUNCT_1:11, A4, FUNCT_3:65;
A25: (hf * [:h,f:]) . p = hf . ([:h,f:] . p) by A22, FUNCT_1:12;
(hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1)
proof
(hf * [:h,f:]) . p in cl_Ball ((0. (TOP-REAL mn)),1) by A16, A20, A22, FUNCT_1:def 3;
then A26: (hf * [:h,f:]) . p in (Sphere ((0. (TOP-REAL mn)),1)) \/ (Ball ((0. (TOP-REAL mn)),1)) by TOPREAL9:18;
assume not (hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1) ; :: thesis: contradiction
then (hf * [:h,f:]) . p in hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] by A26, XBOOLE_0:def 3, A14;
then consider w being object such that
A27: w in dom hf and
A28: w in [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] and
A29: hf . w = (hf * [:h,f:]) . p by FUNCT_1:def 6;
w = [:h,f:] . p by A25, A23, A13, A27, A29, FUNCT_1:def 4;
hence contradiction by A28, A4, A24, A12, ZFMISC_1:87; :: thesis: verum
end;
then p in Fr [:N,M:] by A21, A4, Th5, A15;
then p in ([#] [:N,M:]) \ (Int [:N,M:]) by SUBSET_1:def 4;
hence contradiction by XBOOLE_0:def 5, A1; :: thesis: verum
end;
suppose not y in Int M ; :: thesis: contradiction
then y in ([#] M) \ (Int M) by XBOOLE_0:def 5;
then y in Fr M by SUBSET_1:def 4;
then consider W being a_neighborhood of y, m being Nat, f being Function of (M | W),(Tdisk ((0. (TOP-REAL m)),1)) such that
A30: f is being_homeomorphism and
A31: f . y in Sphere ((0. (TOP-REAL m)),1) by Th5;
A32: y in Int W by CONNSP_2:def 1;
consider U being a_neighborhood of x, n being Nat such that
A33: N | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def2;
reconsider mn = n + m as Nat ;
set TRm = TOP-REAL m;
set TRn = TOP-REAL n;
set TRnm = TOP-REAL mn;
consider h being Function of (N | U),(Tdisk ((0. (TOP-REAL n)),1)) such that
A34: h is being_homeomorphism by A33, T_0TOPSP:def 1;
A35: not f . y in Ball ((0. (TOP-REAL m)),1) by TOPREAL9:19, A31, XBOOLE_0:3;
consider hf being Function of [:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):],(Tdisk ((0. (TOP-REAL mn)),1)) such that
A36: hf is being_homeomorphism and
A37: hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] = Ball ((0. (TOP-REAL mn)),1) by TIETZE_2:19;
set H = hf * [:h,f:];
[:h,f:] is being_homeomorphism by A30, A34, TIETZE_2:15;
then A38: hf * [:h,f:] is being_homeomorphism by A36, TOPS_2:57;
then A39: rng (hf * [:h,f:]) = [#] (Tdisk ((0. (TOP-REAL mn)),1)) by TOPS_2:def 5;
A40: Int W c= W by TOPS_1:16;
A41: Int U c= U by TOPS_1:16;
x in Int U by CONNSP_2:def 1;
then A42: [x,y] in [:U,W:] by A41, A40, A32, ZFMISC_1:87;
n + m in NAT by ORDINAL1:def 12;
then A43: [#] (Tdisk ((0. (TOP-REAL mn)),1)) = cl_Ball ((0. (TOP-REAL mn)),1) by BROUWER:3;
A44: [:(N | U),(M | W):] = [:N,M:] | [:U,W:] by BORSUK_3:22;
then dom (hf * [:h,f:]) = [#] ([:N,M:] | [:U,W:]) by A38, TOPS_2:def 5;
then A45: p in dom (hf * [:h,f:]) by A42, A4, PRE_TOPC:def 5;
then A46: [:h,f:] . p in dom hf by FUNCT_1:11;
dom [:h,f:] = [:(dom h),(dom f):] by FUNCT_3:def 8;
then A47: [:h,f:] . (x,y) = [(h . x),(f . y)] by A45, FUNCT_1:11, A4, FUNCT_3:65;
A48: (hf * [:h,f:]) . p = hf . ([:h,f:] . p) by A45, FUNCT_1:12;
(hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1)
proof
(hf * [:h,f:]) . p in cl_Ball ((0. (TOP-REAL mn)),1) by A39, A43, A45, FUNCT_1:def 3;
then A49: (hf * [:h,f:]) . p in (Sphere ((0. (TOP-REAL mn)),1)) \/ (Ball ((0. (TOP-REAL mn)),1)) by TOPREAL9:18;
assume not (hf * [:h,f:]) . p in Sphere ((0. (TOP-REAL mn)),1) ; :: thesis: contradiction
then (hf * [:h,f:]) . p in hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] by A49, XBOOLE_0:def 3, A37;
then consider w being object such that
A50: w in dom hf and
A51: w in [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] and
A52: hf . w = (hf * [:h,f:]) . p by FUNCT_1:def 6;
w = [:h,f:] . p by A48, A46, A36, A50, A52, FUNCT_1:def 4;
hence contradiction by A51, A4, A47, A35, ZFMISC_1:87; :: thesis: verum
end;
then p in Fr [:N,M:] by A44, A4, Th5, A38;
then p in ([#] [:N,M:]) \ (Int [:N,M:]) by SUBSET_1:def 4;
hence contradiction by XBOOLE_0:def 5, A1; :: thesis: verum
end;
end;
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:(Int N),(Int M):] or z in Int [:N,M:] )
assume A53: z in [:(Int N),(Int M):] ; :: thesis: z in Int [:N,M:]
then consider x, y being object such that
A54: x in Int N and
A55: y in Int M and
A56: z = [x,y] by ZFMISC_1:def 2;
reconsider x = x as Point of N by A54;
consider U being a_neighborhood of x, n being Nat such that
A57: N | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A54, Def4;
reconsider y = y as Point of M by A55;
consider W being a_neighborhood of y, m being Nat such that
A58: M | W, Tball ((0. (TOP-REAL m)),1) are_homeomorphic by A55, Def4;
reconsider p = z as Point of [:N,M:] by A53;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
reconsider mn = m + n as Nat ;
[:(N | U),(M | W):],(TOP-REAL mn) | (Ball ((0. (TOP-REAL mn)),1)) are_homeomorphic by A57, A58, TIETZE_2:20;
then [:N,M:] | [:U,W:], Tball ((0. (TOP-REAL mn)),1) are_homeomorphic by BORSUK_3:22;
hence z in Int [:N,M:] by Def4, A56; :: thesis: verum