Nuprl Lemma : count_bsublist_a
∀s:DSet. ∀as,bs:|s| List. (↑bsublist(s;as;bs) ⇐⇒ ∀c:|s|. ((c #∈ as) ≤ (c #∈ bs)))
Proof
Definitions occuring in Statement :
bsublist: bsublist(s;as;bs),
count: a #∈ as,
list: T List,
assert: ↑b,
le: A ≤ B,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
dset: DSet,
set_car: |p|
Definitions unfolded in proof :
guard: {T}
Lemmas referenced :
count_bsublist
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
hypothesis
Latex:
\mforall{}s:DSet. \mforall{}as,bs:|s| List. (\muparrow{}bsublist(s;as;bs) \mLeftarrow{}{}\mRightarrow{} \mforall{}c:|s|. ((c \#\mmember{} as) \mleq{} (c \#\mmember{} bs)))
Date html generated:
2016_05_16-AM-07_41_29
Last ObjectModification:
2015_12_28-PM-05_41_47
Theory : list_2
Home
Index