Nuprl Lemma : assert-fpf-is-empty
∀[A:Type]. ∀[B:A ─→ Type]. ∀[f:x:A fp-> B[x]]. uiff(↑fpf-is-empty(f);f = ⊗ ∈ x:A fp-> B[x])
Proof
Definitions occuring in Statement :
fpf-is-empty: fpf-is-empty(f),
fpf-empty: ⊗,
fpf: a:A fp-> B[a],
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
so_apply: x[s],
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
eq_int_wf,
length_wf,
assert_of_eq_int,
length_of_null_list,
nil_wf,
and_wf,
equal_wf,
list_wf,
l_member_wf,
pi1_wf_top,
subtype_rel_product,
top_wf,
subtype_top,
iff_weakening_equal,
assert_wf,
assert_witness,
equal-wf-T-base,
fpf_wf,
length_zero,
null_nil_lemma,
btrue_wf,
member-implies-null-eq-bfalse,
null_wf3,
subtype_rel_list,
btrue_neq_bfalse,
set_wf
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[f:x:A fp-> B[x]]. uiff(\muparrow{}fpf-is-empty(f);f = \motimes{})
Date html generated:
2015_07_17-AM-09_16_11
Last ObjectModification:
2015_02_04-PM-05_07_02
Home
Index