### Nuprl Lemma : distinct-representatives

`∀k:ℕ`
`  ∀[A:Type]`
`    (A ~ ℕk`
`    `` (∀[E:A ⟶ A ⟶ ℙ]`
`          (EquivRel(A;x,y.E[x;y])`
`          `` (∀x,y:A.  Dec(E[x;y]))`
`          `` (∃L:A List. ((∀a,b∈L.  ¬E[a;b]) ∧ (∀a:A. (∃b∈L. E[a;b])) ∧ (||L|| ≤ k))))))`

Proof

Definitions occuring in Statement :  equipollent: `A ~ B` pairwise: `(∀x,y∈L.  P[x; y])` l_exists: `(∃x∈L. P[x])` length: `||as||` list: `T List` equiv_rel: `EquivRel(T;x,y.E[x; y])` int_seg: `{i..j-}` nat: `ℕ` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  ge: `i ≥ j ` equipollent: `A ~ B` it: `⋅` nil: `[]` list_ind: list_ind length: `||as||` less_than': `less_than'(a;b)` le: `A ≤ B` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` cand: `A c∧ B` rev_implies: `P `` Q` true: `True` squash: `↓T` iff: `P `⇐⇒` Q` nat: `ℕ` sq_type: `SQType(T)` guard: `{T}` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` or: `P ∨ Q` decidable: `Dec(P)` prop: `ℙ` top: `Top` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` implies: `P `` Q` not: `¬A` uimplies: `b supposing a` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` member: `t ∈ T` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` refl: `Refl(T;x,y.E[x; y])` equiv_rel: `EquivRel(T;x,y.E[x; y])` istype: `istype(T)` trans: `Trans(T;x,y.E[x; y])` sym: `Sym(T;x,y.E[x; y])` pairwise: `(∀x,y∈L.  P[x; y])` less_than: `a < b` select: `L[n]` cons: `[a / b]` uiff: `uiff(P;Q)` nat_plus: `ℕ+` l_exists: `(∃x∈L. P[x])`
Lemmas referenced :  istype-nat int_term_value_add_lemma itermAdd_wf primrec-wf2 le_wf l_member_wf l_exists_wf not_wf list_wf exists_wf all_wf subtype_rel_universe1 uall_wf guard_wf equiv_rel_wf decidable_wf equipollent-partition nat_properties equipollent_inversion length_wf pairwise_wf2 istype-false pairwise-nil nil_wf iff_weakening_equal istype-universe true_wf squash_wf equipollent_wf equipollent-zero subtype_rel_self istype-less_than istype-le decidable__lt decidable__le int_term_value_subtract_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermSubtract_wf intformeq_wf intformnot_wf int_subtype_base set_subtype_base subtype_base_sq subtract_wf decidable__equal_int int_seg_wf int_formula_prop_wf int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma istype-void int_formula_prop_and_lemma istype-int intformle_wf itermConstant_wf itermVar_wf intformless_wf intformand_wf full-omega-unsat int_seg_properties subtype_rel_dep_function subtype_rel_list cons_wf length_of_cons_lemma select-cons-tl select_wf false_wf add-is-int-iff nat_plus_properties length_wf_nat add_nat_plus l_exists_cons
Rules used in proof :  addEquality Error :setIsType,  productEquality functionEquality closedConclusion Error :functionIsType,  baseClosed imageMemberEquality universeEquality Error :inhabitedIsType,  imageElimination intEquality cumulativity Error :isect_memberFormation_alt,  hypothesis_subsumption Error :productIsType,  Error :dependent_set_memberEquality_alt,  applyLambdaEquality equalitySymmetry equalityTransitivity because_Cache instantiate applyEquality unionElimination Error :universeIsType,  independent_pairFormation sqequalRule voidElimination Error :isect_memberEquality_alt,  dependent_functionElimination int_eqEquality Error :lambdaEquality_alt,  Error :dependent_pairFormation_alt,  independent_functionElimination approximateComputation independent_isectElimination productElimination rename setElimination hypothesis hypothesisEquality natural_numberEquality isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut Error :lambdaFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution setEquality Error :equalityIstype,  baseApply promote_hyp pointwiseFunctionality Error :inrFormation_alt

Latex:
\mforall{}k:\mBbbN{}
\mforall{}[A:Type]
(A  \msim{}  \mBbbN{}k
{}\mRightarrow{}  (\mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}]
(EquivRel(A;x,y.E[x;y])
{}\mRightarrow{}  (\mforall{}x,y:A.    Dec(E[x;y]))
{}\mRightarrow{}  (\mexists{}L:A  List.  ((\mforall{}a,b\mmember{}L.    \mneg{}E[a;b])  \mwedge{}  (\mforall{}a:A.  (\mexists{}b\mmember{}L.  E[a;b]))  \mwedge{}  (||L||  \mleq{}  k))))))

Date html generated: 2019_06_20-PM-02_17_59
Last ObjectModification: 2019_01_25-PM-02_44_36

Theory : equipollence!!cardinality!

Home Index