Nuprl Lemma : pv11_p1_about_threshold
∀[T:Type]. ∀[as,bs:bag(T)]. (#(as) < (#(as + bs) + 1) ÷ 2 ⇒ #(as) < #(bs))
Proof
Definitions occuring in Statement :
less_than: a < b,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
divide: n ÷ m,
add: n + m,
natural_number: $n,
universe: Type,
bag-size: #(bs),
bag-append: as + bs,
bag: bag(T)
Lemmas :
bag-size-append,
add-plus-1-div-2-implies-lt,
bag-size_wf,
less_than_wf,
nat_wf,
bag-append_wf,
not-equal-2,
decidable__le,
le_wf,
false_wf,
not-le-2,
condition-implies-le,
add-commutes,
add-associates,
minus-add,
zero-add,
add-swap,
or_wf,
member-less_than,
bag_wf
Latex:
\mforall{}[T:Type]. \mforall{}[as,bs:bag(T)]. (\#(as) < (\#(as + bs) + 1) \mdiv{} 2 {}\mRightarrow{} \#(as) < \#(bs))
Date html generated:
2015_07_23-PM-04_49_06
Last ObjectModification:
2015_01_29-AM-09_49_40
Home
Index