Nuprl Lemma : combinations-list
∀[A:Type]. ∀n:ℕ. (A ~ ℕn ⇒ (∀k:ℕ. ∃C:A List List. ∀L:A List. ((L ∈ C) ⇐⇒ (||L|| = k ∈ ℤ) ∧ no_repeats(A;L))))
Proof
Definitions occuring in Statement :
equipollent: A ~ B,
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
length: ||as||,
list: T List,
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
nat: ℕ,
exists: ∃x:A. B[x],
uimplies: b supposing a,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
subtype_rel: A ⊆r B,
combination: Combination(n;T),
prop: ℙ,
cand: A c∧ B,
so_lambda: λ2x.t[x],
so_apply: x[s],
l_member: (x ∈ l),
ge: i ≥ j ,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
false: False,
not: ¬A,
top: Top,
sq_stable: SqStable(P),
squash: ↓T,
guard: {T}
Lemmas referenced :
nat_wf,
equipollent_wf,
int_seg_wf,
combinations_wf,
combination_wf,
combinations_wf_int,
count-combinations,
equipollent_functionality_wrt_equipollent,
combination_functionality,
equipollent_weakening_ext-eq,
ext-eq_weakening,
equipollent-iff-list,
subtype_rel_list,
list_wf,
no_repeats_witness,
l_member_wf,
equal_wf,
length_wf,
no_repeats_wf,
all_wf,
iff_wf,
length_wf_nat,
select_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,
sq_stable__no_repeats,
equal_functionality_wrt_subtype_rel2,
less_than_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
cumulativity,
hypothesisEquality,
natural_numberEquality,
setElimination,
rename,
universeEquality,
dependent_pairFormation,
because_Cache,
dependent_functionElimination,
independent_functionElimination,
independent_isectElimination,
productElimination,
applyEquality,
lambdaEquality,
sqequalRule,
independent_pairFormation,
productEquality,
intEquality,
dependent_set_memberEquality,
unionElimination,
int_eqEquality,
isect_memberEquality,
voidElimination,
voidEquality,
computeAll,
equalityTransitivity,
equalitySymmetry,
hyp_replacement,
applyLambdaEquality,
imageMemberEquality,
baseClosed,
imageElimination,
promote_hyp
Latex:
\mforall{}[A:Type]
\mforall{}n:\mBbbN{}. (A \msim{} \mBbbN{}n {}\mRightarrow{} (\mforall{}k:\mBbbN{}. \mexists{}C:A List List. \mforall{}L:A List. ((L \mmember{} C) \mLeftarrow{}{}\mRightarrow{} (||L|| = k) \mwedge{} no\_repeats(A;L))))
Date html generated:
2018_05_21-PM-08_10_27
Last ObjectModification:
2017_07_26-PM-05_46_01
Theory : general
Home
Index