Nuprl Lemma : fpf-dom-compose

[x:Top]. ∀[f:a:Top fp-> Top]. ∀[g,eq:Top].  (x ∈ dom(g f) x ∈ dom(f))


Proof




Definitions occuring in Statement :  fpf-compose: f fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] uall: [x:A]. B[x] top: Top sqequal: t
Lemmas :  fpf_dom_compose_lemma top_wf fpf_wf
\mforall{}[x:Top].  \mforall{}[f:a:Top  fp->  Top].  \mforall{}[g,eq:Top].    (x  \mmember{}  dom(g  o  f)  \msim{}  x  \mmember{}  dom(f))



Date html generated: 2015_07_17-AM-11_11_33
Last ObjectModification: 2015_01_28-AM-07_42_56

Home Index