### Nuprl Lemma : fpf-sub-join-right2

`∀[A:Type]. ∀[B,C:A ─→ Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]].`
`  g ⊆ f ⊕ g supposing ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) `` ((B[x] ⊆r C[x]) c∧ (f(x) = g(x) ∈ C[x])))`

Proof

Definitions occuring in Statement :  fpf-join: `f ⊕ g` fpf-sub: `f ⊆ g` fpf-ap: `f(x)` fpf-dom: `x ∈ dom(f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` assert: `↑b` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` cand: `A c∧ B` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T`
Lemmas :  assert_witness fpf-dom_wf fpf-join_wf top_wf assert_wf all_wf subtype-fpf2 subtype_top subtype_rel_wf fpf-ap_wf fpf_wf deq_wf fpf-join-dom2 bool_wf equal-wf-T-base bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot
\mforall{}[A:Type].  \mforall{}[B,C:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[g:a:A  fp->  C[a]].
g  \msubseteq{}  f  \moplus{}  g  supposing  \mforall{}x:A.  (((\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (\muparrow{}x  \mmember{}  dom(g)))  {}\mRightarrow{}  ((B[x]  \msubseteq{}r  C[x])  c\mwedge{}  (f(x)  =  g(x))))

Date html generated: 2015_07_17-AM-09_20_35
Last ObjectModification: 2015_01_28-AM-07_49_29

Home Index