environ
vocabularies HIDDEN, FUNCT_1, RELAT_1, FUNCOP_1, FUNCT_5, FUNCT_6, XBOOLE_0, TARSKI, FUNCT_2, PBOOLE, ZFMISC_1, SUBSET_1, CARD_3, MCART_1, MONOID_0, STRUCT_0, REWRITE1, WAYBEL_0, NEWTON, ORDERS_2, YELLOW_0, BINOP_1, GROUP_6, SEQM_3, XXREAL_0, CAT_1, FUNCT_3, CARD_1, YELLOW_1, RLVECT_2, PRE_TOPC, WAYBEL26, WAYBEL24, WAYBEL25, ORDINAL2, RCOMP_1, WELLORD2, WELLORD1, RELAT_2, WAYBEL11, WAYBEL_9, WAYBEL17, YELLOW_9, EQREL_1, WAYBEL18, PROB_1, WAYBEL_1, WAYBEL_8, RLVECT_3, LATTICES, BORSUK_1, WAYBEL27;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, TOLER_1, MCART_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4, FUNCT_5, ORDINAL1, NUMBERS, CARD_3, FUNCOP_1, FUNCT_6, ORDERS_1, MONOID_0, PRALG_1, QUANTAL1, FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, ORDERS_2, CANTOR_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11, YELLOW_9, WAYBEL17, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16, WAYBEL26;
definitions TARSKI, FUNCT_1, MONOID_0, WAYBEL_0, FUNCOP_1, WAYBEL_1, XBOOLE_0;
theorems YELLOW_1, CARD_3, FUNCT_2, FUNCT_1, PRE_TOPC, TARSKI, PRALG_1, FUNCOP_1, YELLOW_0, WELLORD1, WAYBEL17, WAYBEL10, TOPS_2, TOPS_3, YELLOW_9, WAYBEL24, WAYBEL26, WAYBEL_0, RELSET_1, ORDERS_2, RELAT_1, FUNCT_6, YELLOW14, WAYBEL18, WAYBEL20, WAYBEL25, WAYBEL_1, WAYBEL15, QUANTAL1, WAYBEL14, WAYBEL13, YELLOW16, ZFMISC_1, FUNCT_5, FUNCT_3, YELLOW_2, WAYBEL_3, WAYBEL_8, YELLOW_3, FUNCT_4, WAYBEL21, XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0, CARD_1;
schemes FUNCT_2, PBOOLE, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, TOPS_1, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, WAYBEL_2, WAYBEL_3, WAYBEL_8, WAYBEL10, WAYBEL14, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL19, WAYBEL24, WAYBEL25, YELLOW16, RELSET_1, XTUPLE_0, FUNCT_5;
constructors HIDDEN, DOMAIN_1, TOLER_1, FUNCT_6, TOPS_2, CANTOR_1, MONOID_0, QUANTAL1, ORDERS_3, WAYBEL_6, WAYBEL_8, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL24, YELLOW16, WAYBEL26, RELSET_1, WAYBEL20, FUNCT_5, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities BINOP_1, YELLOW_2, STRUCT_0, ORDINAL1;
expansions TARSKI, FUNCT_1, WAYBEL_0, WAYBEL_1;
definition
let S1,
S2,
T1,
T2 be non
empty reflexive antisymmetric RelStr ;
let f be
Function of
S1,
S2;
assume A1:
f is
directed-sups-preserving
;
let g be
Function of
T1,
T2;
assume A2:
g is
directed-sups-preserving
;
existence
ex b1 being Function of (UPS (S2,T1)),(UPS (S1,T2)) st
for h being directed-sups-preserving Function of S2,T1 holds b1 . h = (g * h) * f
uniqueness
for b1, b2 being Function of (UPS (S2,T1)),(UPS (S1,T2)) st ( for h being directed-sups-preserving Function of S2,T1 holds b1 . h = (g * h) * f ) & ( for h being directed-sups-preserving Function of S2,T1 holds b2 . h = (g * h) * f ) holds
b1 = b2
end;
::
deftheorem Def5 defines
UPS WAYBEL27:def 5 :
for S1, S2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of S1,S2 st f is directed-sups-preserving holds
for g being Function of T1,T2 st g is directed-sups-preserving holds
for b7 being Function of (UPS (S2,T1)),(UPS (S1,T2)) holds
( b7 = UPS (f,g) iff for h being directed-sups-preserving Function of S2,T1 holds b7 . h = (g * h) * f );
theorem Th28:
for
S1,
S2,
S3,
T1,
T2,
T3 being non
empty Poset for
f1 being
directed-sups-preserving Function of
S2,
S3 for
f2 being
directed-sups-preserving Function of
S1,
S2 for
g1 being
directed-sups-preserving Function of
T1,
T2 for
g2 being
directed-sups-preserving Function of
T2,
T3 holds
(UPS (f2,g2)) * (UPS (f1,g1)) = UPS (
(f1 * f2),
(g2 * g1))
Lm1:
now for M being non empty set
for X, Y being non empty Poset
for f being directed-sups-preserving Function of X,(Y |^ M) holds
( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )
let M be non
empty set ;
for X, Y being non empty Poset
for f being directed-sups-preserving Function of X,(Y |^ M) holds
( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )let X,
Y be non
empty Poset;
for f being directed-sups-preserving Function of X,(Y |^ M) holds
( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )let f be
directed-sups-preserving Function of
X,
(Y |^ M);
( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )
the
carrier of
(Y |^ M) = Funcs (
M, the
carrier of
Y)
by YELLOW_1:28;
then A1:
rng f c= Funcs (
M, the
carrier of
Y)
;
dom f = the
carrier of
X
by FUNCT_2:def 1;
hence
f in Funcs ( the
carrier of
X,
(Funcs (M, the carrier of Y)))
by A1, FUNCT_2:def 2;
( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )then
commute f in Funcs (
M,
(Funcs ( the carrier of X, the carrier of Y)))
by FUNCT_6:55;
then
ex
g being
Function st
(
commute f = g &
dom g = M &
rng g c= Funcs ( the
carrier of
X, the
carrier of
Y) )
by FUNCT_2:def 2;
hence
(
rng (commute f) c= Funcs ( the
carrier of
X, the
carrier of
Y) &
dom (commute f) = M )
;
verum
end;
:: preservation of composition