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:
2016_05_17-AM-07_48_27
Last ObjectModification:
2012_02_25-PM-03_03_09
Theory : event-ordering
Home
Index