### 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