Nuprl Lemma : count-unordered-combinations

    (T ~ ℕn
     (UnorderedCombination(m;T) ~ ℕchoose(n;m) supposing m ≤ n ∧ UnorderedCombination(m;T) ~ ℕsupposing n < m))

This theorem is one of freek's list of 100 theorems


Definitions occuring in Statement :  unordered-combination: UnorderedCombination(n;T) equipollent: B int_seg: {i..j-} nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] implies:  Q and: P ∧ Q natural_number: $n universe: Type choose: choose(n;i)
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q cand: c∧ B uimplies: supposing a member: t ∈ T le: A ≤ B not: ¬A false: False nat: prop: int_iseg: {i...j} ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q unordered-combination: UnorderedCombination(n;T) bag-no-repeats: bag-no-repeats(T;bs) squash: T bag-size: #(bs) int_seg: {i..j-} guard: {T} lelt: i ≤ j < k inject: Inj(A;B;f) no_repeats: no_repeats(T;l) less_than': less_than'(a;b) so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  less_than'_wf le_wf member-less_than less_than_wf equipollent_wf int_seg_wf nat_wf unordered-combination_wf choose_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf equipollent-choose equipollent-zero equipollent_functionality_wrt_equipollent unordered-combination_functionality equipollent_weakening_ext-eq ext-eq_weakening equal_wf bag-size_wf pigeon-hole select_wf int_seg_properties decidable__lt intformless_wf intformeq_wf int_formula_prop_less_lemma int_formula_prop_eq_lemma decidable__equal_int_seg int_seg_subtype_nat false_wf set_wf lelt_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality voidElimination extract_by_obid isectElimination setElimination rename hypothesis axiomEquality equalityTransitivity equalitySymmetry independent_pairFormation because_Cache independent_isectElimination cumulativity natural_numberEquality universeEquality dependent_set_memberEquality unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidEquality computeAll productEquality applyEquality independent_functionElimination imageElimination hyp_replacement Error :applyLambdaEquality

        (T  \msim{}  \mBbbN{}n
        {}\mRightarrow{}  (UnorderedCombination(m;T)  \msim{}  \mBbbN{}choose(n;m)  supposing  m  \mleq{}  n
              \mwedge{}  UnorderedCombination(m;T)  \msim{}  \mBbbN{}0  supposing  n  <  m))

Date html generated: 2016_10_25-AM-11_32_25
Last ObjectModification: 2016_07_12-AM-07_36_54

Theory : bags_2

Home Index