Nuprl Lemma : cardinality-le-no_repeats-length

[T:Type]. ∀[k:ℕ]. ∀[L:T List].  (||L|| ≤ k) supposing (no_repeats(T;L) and |T| ≤ k)


Definitions occuring in Statement :  cardinality-le: |T| ≤ n no_repeats: no_repeats(T;l) length: ||as|| list: List nat: uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a cardinality-le: |T| ≤ n exists: x:A. B[x] le: A ≤ B and: P ∧ Q not: ¬A implies:  Q false: False nat: prop: surject: Surj(A;B;f) so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] pi1: fst(t) int_seg: {i..j-} guard: {T} ge: i ≥  lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top less_than: a < b squash: T inject: Inj(A;B;f) no_repeats: no_repeats(T;l) subtype_rel: A ⊆B less_than': less_than'(a;b)
Lemmas referenced :  less_than'_wf length_wf no_repeats_wf cardinality-le_wf list_wf nat_wf exists_wf int_seg_wf equal_wf all_wf pigeon-hole length_wf_nat select_wf int_seg_properties 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 decidable__lt intformless_wf int_formula_prop_less_lemma set_wf lelt_wf decidable__equal_int_seg int_seg_subtype_nat false_wf le_wf intformeq_wf int_formula_prop_eq_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality because_Cache extract_by_obid isectElimination setElimination rename hypothesis cumulativity axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination universeEquality promote_hyp natural_numberEquality applyEquality functionExtensionality dependent_pairFormation lambdaFormation independent_functionElimination independent_isectElimination unionElimination int_eqEquality intEquality voidEquality independent_pairFormation computeAll imageElimination hyp_replacement Error :applyLambdaEquality,  dependent_set_memberEquality

\mforall{}[T:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[L:T  List].    (||L||  \mleq{}  k)  supposing  (no\_repeats(T;L)  and  |T|  \mleq{}  k)

Date html generated: 2016_10_21-AM-10_12_40
Last ObjectModification: 2016_07_12-AM-05_30_28

Theory : list_1

Home Index