Nuprl Definition : sublist*

sublist*(T;as;bs) ==  ∀cs:T List. (cs ⊆ as ⇒ l_subset(T;cs;bs) ⇒ cs ⊆ bs)


Definitions occuring in Statement :  l_subset: l_subset(T;as;bs),  sublist: L1 ⊆ L2,  list: T List,  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  list: T List,  implies: P ⇒ Q,  l_subset: l_subset(T;as;bs),  sublist: L1 ⊆ L2
FDL editor aliases :  sublist*
Latex:
sublist*(T;as;bs)  ==    \mforall{}cs:T  List.  (cs  \msubseteq{}  as  {}\mRightarrow{}  l\_subset(T;cs;bs)  {}\mRightarrow{}  cs  \msubseteq{}  bs)


Date html generated: 2016_05_15-PM-02_06_33
Last ObjectModification: 2015_09_23-AM-07_37_58

Theory : list!


Home Index