Nuprl Definition : single-valued-list
single-valued-list(L;T) == ∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ (x = y ∈ T))
Definitions occuring in Statement :
l_member: (x ∈ l),
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
l_member: (x ∈ l),
equal: s = t ∈ T
FDL editor aliases :
single-valued-list
Latex:
single-valued-list(L;T) == \mforall{}x,y:T. ((x \mmember{} L) {}\mRightarrow{} (y \mmember{} L) {}\mRightarrow{} (x = y))
Date html generated:
2016_05_14-PM-03_01_33
Last ObjectModification:
2015_09_22-PM-05_58_16
Theory : list_1
Home
Index