### Nuprl Lemma : compose-fpf_wf

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

Proof

Definitions occuring in Statement :  compose-fpf: `compose-fpf(a;b;f)` fpf: `a:A fp-> B[a]` outl: `outl(x)` assert: `↑b` isl: `isl(x)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` unit: `Unit` member: `t ∈ T` apply: `f a` function: `x:A ─→ B[x]` union: `left + right` universe: `Type` equal: `s = t ∈ T`
Lemmas :  mapfilter_wf fpf-domain_wf subtype-fpf2 top_wf subtype_top isl_wf unit_wf2 assert_wf outl_wf member_map_filter l_member_wf squash_wf true_wf list_wf iff_weakening_equal all_wf assert_elim bfalse_wf and_wf equal_wf btrue_neq_bfalse fpf_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].
compose-fpf(a;b;f)  \mmember{}  y:C  fp->  B[b  y]  supposing  \mforall{}y:A.  ((\muparrow{}isl(a  y))  {}\mRightarrow{}  ((b  outl(a  y))  =  y))

Date html generated: 2015_07_17-AM-11_11_43
Last ObjectModification: 2015_02_04-PM-05_06_42

Home Index