Nuprl Definition : l_disjoint
l_disjoint(T;l1;l2) == ∀x:T. (¬((x ∈ l1) ∧ (x ∈ l2)))
Definitions occuring in Statement :
l_member: (x ∈ l),
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
l_member: (x ∈ l)
FDL editor aliases :
l_disjoint
Latex:
l\_disjoint(T;l1;l2) == \mforall{}x:T. (\mneg{}((x \mmember{} l1) \mwedge{} (x \mmember{} l2)))
Date html generated:
2016_05_14-AM-07_55_16
Last ObjectModification:
2015_09_22-PM-05_54_12
Theory : list_1
Home
Index