Nuprl Definition : one-one
one-one(A;B;R) == ∀x:A. ∀y,z:B. ((R x y) ⇒ (R x z) ⇒ (y = z ∈ B))
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
one-one
Latex:
one-one(A;B;R) == \mforall{}x:A. \mforall{}y,z:B. ((R x y) {}\mRightarrow{} (R x z) {}\mRightarrow{} (y = z))
Date html generated:
2016_05_14-PM-03_55_53
Last ObjectModification:
2015_09_22-PM-06_01_51
Theory : relations2
Home
Index