### Nuprl Lemma : compose-fpf-dom

`∀[A:Type]. ∀[B:A ─→ Type].`
`  ∀f:x:A fp-> B[x]`
`    ∀[C:Type]`
`      ∀a:A ─→ (C?). ∀b:C ─→ A. ∀y:C.`
`        ((y ∈ fpf-domain(compose-fpf(a;b;f))) `⇐⇒` ∃x:A. ((x ∈ fpf-domain(f)) ∧ ((↑isl(a x)) c∧ (y = outl(a x) ∈ C))))`

Proof

Definitions occuring in Statement :  compose-fpf: `compose-fpf(a;b;f)` fpf-domain: `fpf-domain(f)` fpf: `a:A fp-> B[a]` l_member: `(x ∈ l)` outl: `outl(x)` assert: `↑b` isl: `isl(x)` uall: `∀[x:A]. B[x]` cand: `A c∧ B` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` unit: `Unit` apply: `f a` function: `x:A ─→ B[x]` union: `left + right` universe: `Type` equal: `s = t ∈ T`
Lemmas :  unit_wf2 fpf_wf exists_wf l_member_wf assert_wf isl_wf assert_elim and_wf equal_wf bfalse_wf btrue_neq_bfalse member_map_filter outl_wf mapfilter_wf iff_wf
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
\mforall{}f:x:A  fp->  B[x]
\mforall{}[C:Type]
\mforall{}a:A  {}\mrightarrow{}  (C?).  \mforall{}b:C  {}\mrightarrow{}  A.  \mforall{}y:C.
((y  \mmember{}  fpf-domain(compose-fpf(a;b;f)))
\mLeftarrow{}{}\mRightarrow{}  \mexists{}x:A.  ((x  \mmember{}  fpf-domain(f))  \mwedge{}  ((\muparrow{}isl(a  x))  c\mwedge{}  (y  =  outl(a  x)))))

Date html generated: 2015_07_17-AM-11_11_46
Last ObjectModification: 2015_01_28-AM-07_44_14

Home Index