Nuprl Lemma : count-by-orbits

∀n:ℕ
  ∀[T:Type]
    (T ~ ℕn
    ⇒ (∀f:T ⟶ T
          ∃orbits:T List List
           ((∀o∈orbits.orbit(T;f;o))
           ∧ (∀a:T. (∃o∈orbits. (a ∈ o)))
           ∧ (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
           ∧ no_repeats(T List;orbits)
           ∧ (n = l_sum(map(λo.||o||;orbits)) ∈ ℤ)) 
          supposing Inj(T;T;f)))


Proof



Definitions occuring in Statement :  equipollent: A ~ B,  l_sum: l_sum(L),  orbit: orbit(T;f;L),  pairwise: (∀x,y∈L.  P[x; y]),  l_disjoint: l_disjoint(T;l1;l2),  l_exists: (∃x∈L. P[x]),  l_all: (∀x∈L.P[x]),  no_repeats: no_repeats(T;l),  l_member: (x ∈ l),  length: ||as||,  map: map(f;as),  list: T List,  inject: Inj(A;B;f),  int_seg: {i..j-},  nat: ℕ,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  lambda: λx.A[x],  function: x:A ⟶ B[x],  natural_number: $n,  int: ℤ,  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  implies: P ⇒ Q,  uimplies: b supposing a,  member: t ∈ T,  inject: Inj(A;B;f),  prop: ℙ,  nat: ℕ,  equipollent: A ~ B,  exists: ∃x:A. B[x],  biject: Bij(A;B;f),  and: P ∧ Q,  subtype_rel: A ⊆r B,  int_seg: {i..j-},  decidable: Dec(P),  or: P ∨ Q,  guard: {T},  not: ¬A,  false: False,  finite-type: finite-type(T),  so_lambda: λ2x.t[x],  so_apply: x[s],  cand: A c∧ B,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  ge: i ≥ j ,  satisfiable_int_formula: satisfiable_int_formula(fmla),  top: Top,  lelt: i ≤ j < k,  true: True,  squash: ↓T,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  l_all: (∀x∈L.P[x]),  orbit: orbit(T;f;L)
Lemmas referenced :  equal_wf,  equipollent_inversion,  int_seg_wf,  decidable__int_equal,  not_wf,  orbit-decomp2,  surject_wf,  exists_wf,  l_all_wf,  list_wf,  l_member_wf,  orbit_wf,  all_wf,  l_exists_wf,  pairwise_wf2,  l_disjoint_wf,  no_repeats_wf,  l_sum_wf,  map_wf,  length_wf,  inject_wf,  equipollent_wf,  nat_wf,  nat_properties,  decidable__equal_int,  satisfiable-full-omega-tt,  intformand_wf,  intformnot_wf,  intformeq_wf,  itermVar_wf,  int_formula_prop_and_lemma,  int_formula_prop_not_lemma,  int_formula_prop_eq_lemma,  int_term_value_var_lemma,  int_formula_prop_wf,  decidable__le,  int_seg_properties,  intformle_wf,  itermConstant_wf,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  decidable__lt,  intformless_wf,  int_formula_prop_less_lemma,  lelt_wf,  subtype_rel_list,  top_wf,  length_wf_nat,  concat_wf,  squash_wf,  true_wf,  length-concat,  iff_weakening_equal,  equipollent-nsub,  equipollent_functionality_wrt_equipollent,  equipollent_weakening_ext-eq,  ext-eq_weakening,  equipollent-iff-list,  no_repeats-concat,  member-concat,  l_exists_iff
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation,  isect_memberFormation,  cut,  introduction,  sqequalRule,  sqequalHypSubstitution,  lambdaEquality,  dependent_functionElimination,  thin,  hypothesisEquality,  axiomEquality,  hypothesis,  extract_by_obid,  isectElimination,  cumulativity,  applyEquality,  functionExtensionality,  rename,  natural_numberEquality,  setElimination,  because_Cache,  independent_functionElimination,  productElimination,  unionElimination,  inlFormation,  inrFormation,  hyp_replacement,  equalitySymmetry,  applyLambdaEquality,  intEquality,  voidElimination,  dependent_pairFormation,  functionEquality,  independent_isectElimination,  independent_pairFormation,  productEquality,  setEquality,  universeEquality,  instantiate,  equalityTransitivity,  int_eqEquality,  isect_memberEquality,  voidEquality,  computeAll,  dependent_set_memberEquality,  imageElimination,  imageMemberEquality,  baseClosed
Latex:
\mforall{}n:\mBbbN{}
    \mforall{}[T:Type]
        (T  \msim{}  \mBbbN{}n
        {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T
                    \mexists{}orbits:T  List  List
                      ((\mforall{}o\mmember{}orbits.orbit(T;f;o))
                      \mwedge{}  (\mforall{}a:T.  (\mexists{}o\mmember{}orbits.  (a  \mmember{}  o)))
                      \mwedge{}  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
                      \mwedge{}  no\_repeats(T  List;orbits)
                      \mwedge{}  (n  =  l\_sum(map(\mlambda{}o.||o||;orbits)))) 
                    supposing  Inj(T;T;f)))


Date html generated: 2017_04_17-AM-09_33_28
Last ObjectModification: 2017_02_27-PM-05_32_42

Theory : equipollence!!cardinality!


Home Index