### Nuprl Lemma : fpf-contains-union-join-right2

`∀[A,V:Type]. ∀[B:A ─→ Type].`
`  ∀eq:EqDecider(A). ∀f,h,g:a:A fp-> B[a] List. ∀R:(V List) ─→ V ─→ 𝔹.`
`    fpf-union-compatible(A;V;x.B[x];eq;R;f;g) `` h ⊆⊆ g `` h ⊆⊆ fpf-union-join(eq;R;f;g) `
`    supposing fpf-single-valued(A;eq;x.B[x];V;g) `
`  supposing ∀a:A. (B[a] ⊆r V)`

Proof

Definitions occuring in Statement :  fpf-union-join: `fpf-union-join(eq;R;f;g)` fpf-contains: `f ⊆⊆ g` fpf-single-valued: `fpf-single-valued(A;eq;x.B[x];V;g)` fpf-union-compatible: `fpf-union-compatible(A;C;x.B[x];eq;R;f;g)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` list: `T List` bool: `𝔹` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  l_member_wf fpf-ap_wf list_wf assert_wf fpf-dom_wf subtype-fpf2 top_wf subtype_top fpf-contains_wf fpf-union-compatible_wf fpf-single-valued_wf bool_wf fpf_wf deq_wf all_wf subtype_rel_wf fpf-union-join-dom assert_elim subtype_base_sq bool_subtype_base fpf-union-contains2 fpf-union-join-ap l_all_iff fpf-cap_wf nil_wf fpf-union_wf subtype_rel_dep_function subtype_rel_list subtype_rel_self select_wf sq_stable__le int_seg_wf length_wf equal-wf-T-base bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot
\mforall{}[A,V:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
\mforall{}eq:EqDecider(A).  \mforall{}f,h,g:a:A  fp->  B[a]  List.  \mforall{}R:(V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}.
fpf-union-compatible(A;V;x.B[x];eq;R;f;g)  {}\mRightarrow{}  h  \msubseteq{}\msubseteq{}  g  {}\mRightarrow{}  h  \msubseteq{}\msubseteq{}  fpf-union-join(eq;R;f;g)
supposing  fpf-single-valued(A;eq;x.B[x];V;g)
supposing  \mforall{}a:A.  (B[a]  \msubseteq{}r  V)

Date html generated: 2015_07_17-AM-11_07_49
Last ObjectModification: 2015_01_28-AM-07_48_24

Home Index