Nuprl Lemma : fpf-decompose
∀[A:Type]
∀eq:EqDecider(A)
∀[B:A ─→ Type]
∀f:a:A fp-> B[a]
∃g:a:A fp-> B[a]
∃a:A
∃b:B[a]
((f ⊆ g ⊕ a : b ∧ g ⊕ a : b ⊆ f)
∧ (∀a':A. ¬(a' = a ∈ A) supposing ↑a' ∈ dom(g))
∧ ||fpf-domain(g)|| < ||fpf-domain(f)||)
supposing 0 < ||fpf-domain(f)||
Proof
Definitions occuring in Statement :
fpf-single: x : v,
fpf-join: f ⊕ g,
fpf-sub: f ⊆ g,
fpf-domain: fpf-domain(f),
fpf-dom: x ∈ dom(f),
fpf: a:A fp-> B[a],
deq: EqDecider(T),
length: ||as||,
assert: ↑b,
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
function: x:A ─→ B[x],
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Lemmas :
member-less_than,
length_wf,
fpf-domain_wf,
subtype-fpf2,
top_wf,
subtype_top,
fpf-split,
assert_wf,
bnot_wf,
eqof_wf,
hd_wf,
decidable__le,
false_wf,
not-ge-2,
less-iff-le,
condition-implies-le,
minus-add,
minus-one-mul,
add-swap,
add-associates,
zero-add,
add-commutes,
add_functionality_wrt_le,
add-zero,
le-add-cancel2,
decidable__assert,
list_wf,
less_than_wf,
list-cases,
length_of_nil_lemma,
deq_member_nil_lemma,
product_subtype_list,
reduce_hd_cons_lemma,
length_of_cons_lemma,
deq_member_cons_lemma,
l_member_wf,
iff_transitivity,
bor_wf,
deq-member_wf,
or_wf,
equal_wf,
iff_weakening_uiff,
assert_of_bor,
safe-assert-deq,
assert-deq-member,
member_wf,
fpf-ap_wf,
fpf-sub_wf,
fpf-join_wf,
fpf-single_wf,
all_wf,
fpf-dom_wf,
not_wf,
exists_wf,
fpf_wf,
deq_wf,
fpf-join-sub,
fpf-sub_transitivity,
fpf-sub-reflexive,
assert_of_bnot,
fpf_ap_single_lemma,
fpf-single-dom,
decidable-equal-deq,
eqff_to_assert,
eqtt_to_assert,
bool_subtype_base,
bool_wf,
subtype_base_sq,
bool_cases,
fpf-join-ap-sq,
true_wf,
squash_wf,
assert_functionality_wrt_uiff,
assert_elim,
iff_weakening_equal,
subtype_rel-equal,
fpf-compatible-single-iff,
isect_wf,
fpf-compatible_wf,
fpf-compatible-symmetry,
fpf-join-dom,
fpf-single-dom-sq,
length_sublist,
decidable__equal_int,
proper_sublist_length,
member-fpf-domain
\mforall{}[A:Type]
\mforall{}eq:EqDecider(A)
\mforall{}[B:A {}\mrightarrow{} Type]
\mforall{}f:a:A fp-> B[a]
\mexists{}g:a:A fp-> B[a]
\mexists{}a:A
\mexists{}b:B[a]
((f \msubseteq{} g \moplus{} a : b \mwedge{} g \moplus{} a : b \msubseteq{} f)
\mwedge{} (\mforall{}a':A. \mneg{}(a' = a) supposing \muparrow{}a' \mmember{} dom(g))
\mwedge{} ||fpf-domain(g)|| < ||fpf-domain(f)||)
supposing 0 < ||fpf-domain(f)||
Date html generated:
2015_07_17-AM-11_13_14
Last ObjectModification:
2015_07_16-AM-09_51_25
Home
Index