Nuprl Lemma : zhgrp_to_nat_is_hom

IsMonHom{<ℤ+>↓hgrp,<ℕ,+>}(λn.nat(n))


Proof




Definitions occuring in Statement :  int_hgrp_to_nat: nat(n) nat_add_mon: <ℕ,+> int_add_grp: <ℤ+> hgrp_of_ocgrp: g↓hgrp monoid_hom_p: IsMonHom{M1,M2}(f) lambda: λx.A[x]
Definitions unfolded in proof :  monoid_hom_p: IsMonHom{M1,M2}(f) and: P ∧ Q fun_thru_2op: FunThru2op(A;B;opa;opb;f) uall: [x:A]. B[x] member: t ∈ T nat_add_mon: <ℕ,+> grp_car: |g| pi1: fst(t) grp_op: * pi2: snd(t) infix_ap: y grp_id: e int_hgrp_to_nat: nat(n) hgrp_of_ocgrp: g↓hgrp int_add_grp: <ℤ+> all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: false: False nat: le: A ≤ B less_than': less_than'(a;b) not: ¬A implies:  Q
Lemmas referenced :  le_wf false_wf int_formula_prop_wf int_term_value_constant_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermConstant_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int int_hgrp_to_nat_wf add_nat_wf int_add_grp_wf2 hgrp_of_ocgrp_wf grp_car_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut sqequalRule hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality hypothesisEquality axiomEquality because_Cache dependent_functionElimination natural_numberEquality unionElimination independent_isectElimination dependent_pairFormation lambdaEquality intEquality voidElimination voidEquality computeAll dependent_set_memberEquality equalityTransitivity equalitySymmetry lambdaFormation

Latex:
IsMonHom\{<\mBbbZ{}+>\mdownarrow{}hgrp,<\mBbbN{},+>\}(\mlambda{}n.nat(n))



Date html generated: 2016_05_15-PM-00_19_39
Last ObjectModification: 2016_01_15-PM-11_05_45

Theory : groups_1


Home Index