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))
Proof
Definitions occuring in Statement :
fpf-inv-rename: fpf-inv-rename(r;rinv;f),
fpf: a:A fp-> B[a],
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
unit: Unit,
member: t ∈ T,
apply: f a,
function: x:A ─→ B[x],
union: left + right,
universe: Type,
equal: s = t ∈ T,
inv-rel: inv-rel(A;B;f;finv)
Lemmas :
mapfilter_wf,
isl_wf,
unit_wf2,
assert_wf,
outl_wf,
subtype_rel-equal,
iff_weakening_equal,
l_member_wf,
member_map_filter,
equal_wf,
true_wf,
false_wf
\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
inv-rel(A;C;r;rinv))
Date html generated:
2015_07_17-AM-11_11_17
Last ObjectModification:
2015_02_04-PM-05_06_47
Home
Index