### Nuprl Lemma : fpf-rename-dom

`∀[A,C:Type]. ∀[B:A ─→ Type].`
`  ∀eqa:EqDecider(A). ∀eqc:EqDecider(C). ∀r:A ─→ C. ∀f:a:A fp-> B[a]. ∀c:C.`
`    (↑c ∈ dom(rename(r;f)) `⇐⇒` ∃a:A. ((↑a ∈ dom(f)) c∧ (c = (r a) ∈ C)))`

Proof

Definitions occuring in Statement :  fpf-rename: `rename(r;f)` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` assert: `↑b` 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` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T`
Lemmas :  exists_wf l_member_wf member_map map_wf iff_wf assert_wf deq-member_wf equal_wf
\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
\mforall{}eqa:EqDecider(A).  \mforall{}eqc:EqDecider(C).  \mforall{}r:A  {}\mrightarrow{}  C.  \mforall{}f:a:A  fp->  B[a].  \mforall{}c:C.
(\muparrow{}c  \mmember{}  dom(rename(r;f))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A.  ((\muparrow{}a  \mmember{}  dom(f))  c\mwedge{}  (c  =  (r  a))))

Date html generated: 2015_07_17-AM-11_10_41
Last ObjectModification: 2015_01_28-AM-07_44_24

Home Index