Nuprl Lemma : fpf-rename_wf

`∀[A,C:Type]. ∀[B:A ⟶ Type]. ∀[D:C ⟶ Type]. ∀[eq:EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B[a]].`
`  rename(r;f) ∈ c:C fp-> D[c] supposing ∀a:A. (D[r a] = B[a] ∈ Type)`

Proof

Definitions occuring in Statement :  fpf-rename: `rename(r;f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` fpf: `a:A fp-> B[a]` fpf-rename: `rename(r;f)` pi1: `fst(t)` pi2: `snd(t)` all: `∀x:A. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` guard: `{T}` implies: `P `` Q` subtype_rel: `A ⊆r B` squash: `↓T` true: `True` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` deq: `EqDecider(T)` exists: `∃x:A. B[x]` cand: `A c∧ B` eqof: `eqof(d)` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  set_wf l_member_wf map_wf all_wf equal_wf fpf_wf deq_wf subtype_rel-equal squash_wf true_wf subtype_rel_self iff_weakening_equal hd-filter member_map safe-assert-deq assert_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut sqequalHypSubstitution productElimination thin sqequalRule lambdaFormation introduction extract_by_obid isectElimination hypothesisEquality lambdaEquality hypothesis dependent_pairEquality dependent_functionElimination setEquality functionEquality applyEquality setElimination rename instantiate cumulativity universeEquality dependent_set_memberEquality independent_isectElimination imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality baseClosed independent_functionElimination because_Cache dependent_pairFormation independent_pairFormation productEquality

Latex:
\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(C)].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:a:A  fp->  B[a]].
rename(r;f)  \mmember{}  c:C  fp->  D[c]  supposing  \mforall{}a:A.  (D[r  a]  =  B[a])

Date html generated: 2018_05_21-PM-09_26_42
Last ObjectModification: 2018_05_19-PM-04_37_56

Theory : finite!partial!functions

Home Index