Nuprl Definition : Q-R-glues
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) ∈ Ib_valtype))
Definitions occuring in Statement :
es-E-interface: E(X)
,
es-interface-predicate: {I}
,
eclass-val: X(e)
,
Q-R-pre-preserving: f is Q-R-pre-preserving on P
,
weak-antecedent-surjection: Q ←←= f== P
,
es-E: E
,
inject: Inj(A;B;f)
,
all: ∀x:A. B[x]
,
and: P ∧ Q
,
apply: f a
,
equal: s = t ∈ T
FDL editor aliases :
Q-R-glues
Latex:
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:
2015_07_21-PM-04_07_39
Last ObjectModification:
2012_02_25-PM-03_03_09
Home
Index