Nuprl Lemma : equipollent-choose
∀n,m:ℕ. ((m ≤ n) ⇒ UnorderedCombination(m;ℕn) ~ ℕchoose(n;m))
Proof
Definitions occuring in Statement :
unordered-combination: UnorderedCombination(n;T),
equipollent: A ~ B,
int_seg: {i..j-},
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n,
choose: choose(n;i)
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
uimplies: b supposing a,
not: ¬A,
implies: P ⇒ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
top: Top,
prop: ℙ,
decidable: Dec(P),
or: P ∨ Q,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
guard: {T},
sq_type: SQType(T),
nat: ℕ,
choose: choose(n;i),
ycomb: Y,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
bfalse: ff,
bnot: ¬bb,
assert: ↑b,
le: A ≤ B,
less_than': less_than'(a;b),
ge: i ≥ j ,
int_upper: {i...},
int_iseg: {i...j},
cand: A c∧ B,
unordered-combination: UnorderedCombination(n;T),
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
squash: ↓T,
true: True,
nequal: a ≠ b ∈ T ,
istype: istype(T),
bag-no-repeats: bag-no-repeats(T;bs),
bag-size: #(bs),
bag: bag(T),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
bag-rep: bag-rep(n;x),
bag-co-restrict: (b|¬x),
subtract: n - m,
equipollent: A ~ B,
biject: Bij(A;B;f),
inject: Inj(A;B;f),
respects-equality: respects-equality(S;T),
surject: Surj(A;B;f),
bag-member: x ↓∈ bs,
quotient: x,y:A//B[x; y],
l_member: (x ∈ l),
sq_or: a ↓∨ b,
int-deq: IntDeq,
ext-eq: A ≡ B
Lemmas referenced :
int_seg_properties,
full-omega-unsat,
intformand_wf,
intformless_wf,
itermVar_wf,
itermConstant_wf,
intformle_wf,
istype-int,
int_formula_prop_and_lemma,
istype-void,
int_formula_prop_less_lemma,
int_term_value_var_lemma,
int_term_value_constant_lemma,
int_formula_prop_le_lemma,
int_formula_prop_wf,
int_seg_wf,
decidable__equal_int,
subtract_wf,
subtype_base_sq,
set_subtype_base,
int_subtype_base,
intformnot_wf,
intformeq_wf,
itermSubtract_wf,
int_formula_prop_not_lemma,
int_formula_prop_eq_lemma,
int_term_value_subtract_lemma,
decidable__le,
decidable__lt,
istype-le,
istype-less_than,
subtype_rel_self,
eq_int_wf,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
bool_cases_sqequal,
bool_wf,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
upper_subtype_nat,
istype-false,
nat_properties,
nequal-le-implies,
zero-add,
guard_wf,
all_wf,
nat_wf,
le_wf,
equipollent_wf,
unordered-combination_wf,
choose_wf,
int_seg_subtype_nat,
istype-nat,
primrec-wf2,
itermAdd_wf,
int_term_value_add_lemma,
equipollent-one-iff,
bag_wf,
bag-no-repeats_wf,
equal-wf-base,
bag-size_wf,
empty-bag-no-repeats,
bag_size_empty_lemma,
equal_wf,
squash_wf,
true_wf,
istype-universe,
iff_weakening_equal,
empty-bag_wf,
bag-size-zero,
upto_wf,
list-subtype-bag,
no_repeats_upto,
list_subtype_base,
lelt_wf,
no_repeats_wf,
length_upto,
quotient-member-eq,
list_wf,
permutation_wf,
permutation-equiv,
permutation-when-no_repeats,
decidable__l_member,
decidable__equal_int_seg,
l_member_wf,
member_upto2,
int_upper_properties,
equal-wf-T-base,
equipollent-split,
decidable__squash,
not_wf,
length_wf,
equipollent-partition,
equipollent_same,
equipollent_functionality_wrt_equipollent2,
union_functionality_wrt_equipollent,
equipollent-length,
equipollent_weakening_ext-eq,
ext-eq_weakening,
equipollent-add,
equipollent-nsub,
equipollent-zero,
bag-member_wf,
decidable__bag-member2,
bag-rep-size-restrict,
int-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
single-bag_wf,
bag-size-restrict,
subtype_rel_bag,
bag-no-repeats-count,
bag-member-count,
primrec1_lemma,
cons_bag_empty_lemma,
bag-restrict-split,
bag-co-restrict_wf,
bag-append_wf,
bag-settype,
intdeq_reduce_lemma,
bag-member-filter,
bnot_wf,
assert_elim,
bfalse_wf,
eq_int_eq_true,
btrue_neq_bfalse,
bag-filter-no-repeats,
int_seg_subtype,
add-is-int-iff,
not-le-2,
condition-implies-le,
add-associates,
minus-add,
minus-one-mul,
add-swap,
minus-one-mul-top,
add-mul-special,
zero-mul,
add-zero,
add-commutes,
le-add-cancel2,
le_witness_for_triv,
bag-size-append,
bag_size_single_lemma,
biject_wf,
subtype_rel_set,
respects-equality-set,
respects-equality-bag,
subtype-base-respects-equality,
bag-append-no-repeats,
bag-single-no-repeats,
bag-no-repeats-supertype,
strong-subtype-set1,
bag-member-single,
bag_to_squash_list,
member-permutation,
non_neg_length,
select_wf,
length_wf_nat,
bag-member-append,
bag-member-strong-subtype,
bag-co-restrict-append,
bag-co-restrict-rep,
empty_bag_append_lemma,
bag-filter-trivial,
iff_transitivity,
assert_wf,
iff_weakening_uiff,
assert_of_bnot,
istype-assert,
bag-no-repeats-subtype,
subtype_rel_list,
equal_functionality_wrt_subtype_rel2,
no_repeats-strong-subtype,
subtype-respects-equality,
satisfiable-full-omega-tt,
false_wf,
member_wf,
equipollent_functionality_wrt_ext-eq-left,
equipollent_functionality_wrt_equipollent
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
thin,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
natural_numberEquality,
hypothesisEquality,
hypothesis,
setElimination,
rename,
productElimination,
independent_isectElimination,
approximateComputation,
independent_functionElimination,
dependent_pairFormation_alt,
lambdaEquality_alt,
int_eqEquality,
dependent_functionElimination,
isect_memberEquality_alt,
voidElimination,
sqequalRule,
independent_pairFormation,
universeIsType,
unionElimination,
applyEquality,
instantiate,
because_Cache,
equalityTransitivity,
equalitySymmetry,
applyLambdaEquality,
dependent_set_memberEquality_alt,
productIsType,
hypothesis_subsumption,
inhabitedIsType,
equalityElimination,
equalityIstype,
promote_hyp,
cumulativity,
functionIsType,
functionEquality,
closedConclusion,
setIsType,
addEquality,
intEquality,
setEquality,
productEquality,
baseClosed,
imageElimination,
universeEquality,
imageMemberEquality,
sqequalBase,
baseApply,
hyp_replacement,
unionEquality,
minusEquality,
multiplyEquality,
isect_memberFormation_alt,
independent_pairEquality,
axiomEquality,
isectIsTypeImplies,
pertypeElimination,
inlFormation_alt,
computeAll,
voidEquality,
isect_memberEquality,
lambdaEquality,
dependent_pairFormation,
lambdaFormation,
dependent_set_memberEquality
Latex:
\mforall{}n,m:\mBbbN{}. ((m \mleq{} n) {}\mRightarrow{} UnorderedCombination(m;\mBbbN{}n) \msim{} \mBbbN{}choose(n;m))
Date html generated:
2019_10_16-AM-11_33_29
Last ObjectModification:
2018_11_28-PM-11_21_57
Theory : bags_2
Home
Index