### Nuprl Lemma : cardinality-le-no_repeats-length

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

Proof

Definitions occuring in Statement :  cardinality-le: `|T| ≤ n` no_repeats: `no_repeats(T;l)` length: `||as||` list: `T List` nat: `ℕ` uimplies: `b 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: `b supposing a` cardinality-le: `|T| ≤ n` exists: `∃x:A. B[x]` le: `A ≤ B` and: `P ∧ Q` not: `¬A` implies: `P `` 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 ≥ j ` 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 ⊆r 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

Latex:
\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