Nuprl Lemma : fpf-inv-rename_wf

[A,C:Type]. ∀[B:A ⟶ Type]. ∀[D:C ⟶ Type]. ∀[rinv:C ⟶ (A?)]. ∀[r:A ⟶ C]. ∀[f:c:C fp-> D[c]].
  (fpf-inv-rename(r;rinv;f) ∈ a:A fp-> B[a]) supposing ((∀a:A. (D[r a] B[a] ∈ Type)) and inv-rel(A;C;r;rinv))


Definitions occuring in Statement :  fpf-inv-rename: fpf-inv-rename(r;rinv;f) fpf: a:A fp-> B[a] inv-rel: inv-rel(A;B;f;finv) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] unit: Unit member: t ∈ T apply: a function: x:A ⟶ B[x] union: left right universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a fpf-inv-rename: fpf-inv-rename(r;rinv;f) fpf: a:A fp-> B[a] pi1: fst(t) pi2: snd(t) prop: so_apply: x[s] so_lambda: λ2x.t[x] all: x:A. B[x] isl: isl(x) compose: g subtype_rel: A ⊆B iff: ⇐⇒ Q and: P ∧ Q implies:  Q exists: x:A. B[x] cand: c∧ B inv-rel: inv-rel(A;B;f;finv) outl: outl(x) not: ¬A false: False assert: b ifthenelse: if then else fi  btrue: tt bfalse: ff
Lemmas referenced :  l_member_wf all_wf equal_wf inv-rel_wf fpf_wf unit_wf2 mapfilter_wf isl_wf assert_wf outl_wf member_map_filter assert_elim and_wf bfalse_wf btrue_neq_bfalse true_wf false_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule dependent_pairEquality functionEquality setEquality hypothesisEquality extract_by_obid isectElimination hypothesis applyEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry instantiate cumulativity lambdaEquality universeEquality isect_memberEquality because_Cache unionEquality functionExtensionality lambdaFormation independent_isectElimination dependent_functionElimination independent_functionElimination dependent_set_memberEquality hyp_replacement applyLambdaEquality unionElimination independent_pairFormation voidElimination inlEquality

\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].  \mforall{}[rinv:C  {}\mrightarrow{}  (A?)].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:c:C  fp->  D[c]].
    (fpf-inv-rename(r;rinv;f)  \mmember{}  a:A  fp->  B[a])  supposing 
          ((\mforall{}a:A.  (D[r  a]  =  B[a]))  and 

Date html generated: 2018_05_21-PM-09_27_28
Last ObjectModification: 2018_05_19-PM-04_38_21

Theory : finite!partial!functions

Home Index