Nuprl Definition : l_subset

l_subset(T;as;bs) ==  ∀x:T. ((x ∈ as) ⇒ (x ∈ bs))


Definitions occuring in Statement :  l_member: (x ∈ l),  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  implies: P ⇒ Q,  l_member: (x ∈ l)
FDL editor aliases :  l_subset
Latex:
l\_subset(T;as;bs)  ==    \mforall{}x:T.  ((x  \mmember{}  as)  {}\mRightarrow{}  (x  \mmember{}  bs))


Date html generated: 2016_05_14-AM-07_53_14
Last ObjectModification: 2015_09_22-PM-05_54_09

Theory : list_1


Home Index