### Nuprl Lemma : fpf-dom-compose

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

Proof

Definitions occuring in Statement :  fpf-compose: `g o f` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` uall: `∀[x:A]. B[x]` top: `Top` sqequal: `s ~ t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` top: `Top` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  fpf_dom_compose_lemma top_wf fpf_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution sqequalTransitivity computationStep dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis isect_memberFormation introduction sqequalAxiom isectElimination hypothesisEquality because_Cache lambdaEquality

Latex:
\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: 2018_05_21-PM-09_27_44
Last ObjectModification: 2018_02_09-AM-10_23_17

Theory : finite!partial!functions

Home Index