g glues Ia:Qa 
f
Ib:Rb ==
({Ia} 
= g== {Ib} 
g is Qa-Rb-pre-preserving on {Ib})
Inj(E(Ib);E;g)
(
e:E(Ib). ((f (g e)) = Ib(e)))
Definitions :
weak-antecedent-surjection: Q = f== P,
Q-R-pre-preserving: f is Q-R-pre-preserving on P,
es-interface-predicate: {I},
and: P Q,
inject: Inj(A;B;f),
es-E: E,
all: x:A. B[x],
es-E-interface: E(X),
equal: s = t,
apply: f a,
eclass-val: X(e)
FDL editor aliases :
Q-R-glues
g glues Ia:Qa {}{}f{}\mrightarrow{} Ib:Rb ==
(\{Ia\} \mleftarrow{}\mleftarrow{}= g== \{Ib\} \mwedge{} g is Qa-Rb-pre-preserving on \{Ib\})
\mwedge{} Inj(E(Ib);E;g)
\mwedge{} (\mforall{}e:E(Ib). ((f (g e)) = Ib(e)))
Date html generated:
2010_08_27-PM-03_18_45
Last ObjectModification:
2010_04_06-PM-12_28_20
Home
Index