Nuprl Definition : p-inject
p-inject(A;B;f) ==
∀x,y:A. ((↑can-apply(f;x)) ⇒ (↑can-apply(f;y)) ⇒ (do-apply(f;x) = do-apply(f;y) ∈ B) ⇒ (x = y ∈ A))
Definitions occuring in Statement :
do-apply: do-apply(f;x),
can-apply: can-apply(f;x),
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
assert: ↑b,
can-apply: can-apply(f;x),
implies: P ⇒ Q,
do-apply: do-apply(f;x),
equal: s = t ∈ T
FDL editor aliases :
p-inject
Latex:
p-inject(A;B;f) ==
\mforall{}x,y:A. ((\muparrow{}can-apply(f;x)) {}\mRightarrow{} (\muparrow{}can-apply(f;y)) {}\mRightarrow{} (do-apply(f;x) = do-apply(f;y)) {}\mRightarrow{} (x = y))
Date html generated:
2016_05_15-PM-03_37_19
Last ObjectModification:
2015_09_23-AM-07_44_22
Theory : general
Home
Index