Nuprl Definition : inject
(basic):: Inj(A;B;f) == ∀a1,a2:A. (((f a1) = (f a2) ∈ B) ⇒ (a1 = a2 ∈ A))
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 :
inject
Latex:
(basic):: Inj(A;B;f) == \mforall{}a1,a2:A. (((f a1) = (f a2)) {}\mRightarrow{} (a1 = a2))
Date html generated:
2016_05_13-PM-04_04_44
Last ObjectModification:
2015_09_22-PM-05_45_50
Theory : fun_1
Home
Index