environ
vocabularies HIDDEN, XBOOLE_0, TARSKI, RELAT_1, PARTFUN1, MCART_1, ZFMISC_1, FUNCT_1, FUNCT_3, SUBSET_1, WAYBEL_0, ORDERS_2, LATTICES, LATTICE3, YELLOW_0, ORDINAL2, EQREL_1, RELAT_2, WAYBEL_3, WAYBEL_2, STRUCT_0, WELLORD1, WAYBEL11, XXREAL_0, REWRITE1, SETFAM_1, PRE_TOPC, RLVECT_3, CANTOR_1, RCOMP_1, CONNSP_2, TOPS_1, TOPS_2, T_0TOPSP, COMPTS_1, YELLOW_9, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, MCART_1, FUNCT_3, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CANTOR_1, CONNSP_2, BORSUK_1, BORSUK_2, T_0TOPSP, WELLORD1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_8, WAYBEL11, YELLOW_9;
definitions TARSKI, FUNCT_1, PRE_TOPC, TOPS_2, BORSUK_1, T_0TOPSP, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_2, WAYBEL_3, WAYBEL11, XBOOLE_0;
theorems FUNCT_1, FUNCT_2, FUNCT_3, RELAT_1, TOPS_1, TOPS_2, TOPS_3, PRE_TOPC, CONNSP_2, BORSUK_1, ZFMISC_1, TARSKI, ORDERS_2, YELLOW_0, YELLOW_2, YELLOW_3, YELLOW_4, WAYBEL_0, WAYBEL_1, WAYBEL_2, YELLOW_7, YELLOW_8, YELLOW_9, WAYBEL_8, WAYBEL_3, TEX_2, SETFAM_1, CANTOR_1, XBOOLE_0, XBOOLE_1, EQREL_1, XTUPLE_0;
schemes ;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, BORSUK_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3, YELLOW_9, PRE_TOPC, TOPS_1, BORSUK_2, FUNCT_2;
constructors HIDDEN, SETFAM_1, TOLER_1, TOPS_1, TOPS_2, T_0TOPSP, CANTOR_1, BORSUK_2, ORDERS_3, YELLOW_4, WAYBEL_3, YELLOW_8, WAYBEL11, YELLOW_9, CONNSP_2, DOMAIN_1, COMPTS_1, WAYBEL_2;
requirements HIDDEN, SUBSET, BOOLE;
equalities LATTICE3, WAYBEL_3, SUBSET_1, BINOP_1, STRUCT_0;
expansions TARSKI, FUNCT_1, PRE_TOPC, LATTICE3, YELLOW_0, WAYBEL_0;
Lm1:
now for S, T, x1, x2 being set st x1 in S & x2 in T holds
<:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1]
let S,
T,
x1,
x2 be
set ;
( x1 in S & x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1] )assume A1:
(
x1 in S &
x2 in T )
;
<:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1]A2:
dom <:(pr2 (S,T)),(pr1 (S,T)):> =
(dom (pr2 (S,T))) /\ (dom (pr1 (S,T)))
by FUNCT_3:def 7
.=
(dom (pr2 (S,T))) /\ [:S,T:]
by FUNCT_3:def 4
.=
[:S,T:] /\ [:S,T:]
by FUNCT_3:def 5
.=
[:S,T:]
;
[x1,x2] in [:S,T:]
by A1, ZFMISC_1:87;
hence <:(pr2 (S,T)),(pr1 (S,T)):> . (
x1,
x2) =
[((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))]
by A2, FUNCT_3:def 7
.=
[x2,((pr1 (S,T)) . (x1,x2))]
by A1, FUNCT_3:def 5
.=
[x2,x1]
by A1, FUNCT_3:def 4
;
verum
end;
theorem Th48:
for
S1,
S2,
T1,
T2 being non
empty TopSpace for
R being
Refinement of
[:S1,T1:],
[:S2,T2:] st the
carrier of
S1 = the
carrier of
S2 & the
carrier of
T1 = the
carrier of
T2 holds
{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is
Basis of
R
theorem Th49:
for
S1,
S2,
T1,
T2 being non
empty TopSpace for
R being
Refinement of
[:S1,T1:],
[:S2,T2:] for
R1 being
Refinement of
S1,
S2 for
R2 being
Refinement of
T1,
T2 st the
carrier of
S1 = the
carrier of
S2 & the
carrier of
T1 = the
carrier of
T2 holds
( the
carrier of
[:R1,R2:] = the
carrier of
R & the
topology of
[:R1,R2:] = the
topology of
R )