Nuprl Lemma : nat_op_mon_hom_1

[g:IMonoid]. ∀[a:|g|].  IsMonHom{<ℕ,+>,g}(λn.(n ⋅ a))


Proof




Definitions occuring in Statement :  nat_add_mon: <ℕ,+> mon_nat_op: n ⋅ e monoid_hom_p: IsMonHom{M1,M2}(f) imon: IMonoid grp_car: |g| uall: [x:A]. B[x] lambda: λx.A[x]
Definitions unfolded in proof :  monoid_hom_p: IsMonHom{M1,M2}(f) fun_thru_2op: FunThru2op(A;B;opa;opb;f) nat_add_mon: <ℕ,+> grp_car: |g| pi1: fst(t) grp_op: * pi2: snd(t) grp_id: e infix_ap: y uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q imon: IMonoid
Lemmas referenced :  mon_nat_op_add nat_wf mon_nat_op_zero grp_car_wf imon_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut independent_pairFormation lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis isect_memberEquality axiomEquality because_Cache productElimination independent_pairEquality setElimination rename

Latex:
\mforall{}[g:IMonoid].  \mforall{}[a:|g|].    IsMonHom\{<\mBbbN{},+>,g\}(\mlambda{}n.(n  \mcdot{}  a))



Date html generated: 2016_05_15-PM-00_18_03
Last ObjectModification: 2015_12_26-PM-11_38_31

Theory : groups_1


Home Index