Nuprl Lemma : fpf-rename-ap

[A,C:Type]. ∀[B:A ⟶ Type]. ∀[eqa:EqDecider(A)]. ∀[eqc:EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B[a]]. ∀[a:A].
  (rename(r;f)(r a) f(a) ∈ B[a]) supposing ((↑a ∈ dom(f)) and Inj(A;C;r))


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

\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{}[a:A].
    (rename(r;f)(r  a)  =  f(a))  supposing  ((\muparrow{}a  \mmember{}  dom(f))  and  Inj(A;C;r))

Date html generated: 2018_05_21-PM-09_26_56
Last ObjectModification: 2018_02_09-AM-10_22_14

Theory : finite!partial!functions

Home Index