Nuprl Lemma : length-eq-lists-diff-elts
∀[T:Type]
∀eq:∀x,y:T. Dec(x = y ∈ T). ∀L1,L2:T List.
(no_repeats(T;L1) ⇒ (||L1|| ≥ ||L2|| ) ⇒ (∃x:T. ((x ∈ L2) ∧ (¬(x ∈ L1)))) ⇒ (∃x:T. ((x ∈ L1) ∧ (¬(x ∈ L2)))))
Proof
Definitions occuring in Statement :
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
length: ||as||,
list: T List,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
ge: i ≥ j ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
universe: Type,
equal: s = t ∈ T
Lemmas :
decidable__l_exists,
not_wf,
l_member_wf,
decidable__not,
decidable__l_member,
l_exists_iff,
not-l_exists,
l_all_iff,
deq-exists,
select_wf,
sq_stable__le,
select_member,
filter_wf5,
bnot_wf,
lelt_wf,
length_wf,
equal_wf,
member_filter,
int_seg_subtype-nat,
false_wf,
less_than_wf,
iff_transitivity,
assert_wf,
eqof_wf,
iff_weakening_uiff,
assert_of_bnot,
safe-assert-deq,
int_seg_wf,
exists_wf,
ge_wf,
no_repeats_wf,
list_wf,
all_wf,
decidable_wf,
zero-le-nat,
non_neg_length,
length_wf_nat,
decidable__equal_int_seg,
le_wf,
nat_wf,
iff_weakening_equal,
squash_wf,
pigeon-hole,
length-filter-decreases,
less_than_transitivity1,
less_than_irreflexivity,
set_wf,
l_exists_wf,
l_exists_functionality
Latex:
\mforall{}[T:Type]
\mforall{}eq:\mforall{}x,y:T. Dec(x = y). \mforall{}L1,L2:T List.
(no\_repeats(T;L1)
{}\mRightarrow{} (||L1|| \mgeq{} ||L2|| )
{}\mRightarrow{} (\mexists{}x:T. ((x \mmember{} L2) \mwedge{} (\mneg{}(x \mmember{} L1))))
{}\mRightarrow{} (\mexists{}x:T. ((x \mmember{} L1) \mwedge{} (\mneg{}(x \mmember{} L2)))))
Date html generated:
2015_07_22-PM-00_17_23
Last ObjectModification:
2015_02_04-PM-04_39_28
Home
Index