Nuprl Lemma : map-map2

[as,f,g:Top].  (map(g;map(f;as)) map(g f;as))


Proof




Definitions occuring in Statement :  map: map(f;as) compose: g uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  map_map top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalAxiom sqequalRule isect_memberEquality because_Cache

Latex:
\mforall{}[as,f,g:Top].    (map(g;map(f;as))  \msim{}  map(g  o  f;as))



Date html generated: 2016_05_14-AM-06_55_52
Last ObjectModification: 2015_12_26-PM-01_15_13

Theory : omega


Home Index