Nuprl Lemma : fpf-join-wf

[A:Type]. ∀[B,C,D:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]]. ∀[eq:EqDecider(A)].
  (f ⊕ g ∈ a:A fp-> D[a]) supposing 
     ((∀a:A. ((↑a ∈ dom(g))  (C[a] ⊆D[a]))) and 
     (∀a:A. ((↑a ∈ dom(f))  (B[a] ⊆D[a]))))


Definitions occuring in Statement :  fpf-join: f ⊕ g fpf-dom: x ∈ dom(f) fpf: a:A fp-> B[a] deq: EqDecider(T) assert: b uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] implies:  Q member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  fpf: a:A fp-> B[a] fpf-join: f ⊕ g pi1: fst(t) all: x:A. B[x] member: t ∈ T top: Top fpf-cap: f(x)?z fpf-dom: x ∈ dom(f) uall: [x:A]. B[x] implies:  Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a prop: iff: ⇐⇒ Q and: P ∧ Q or: P ∨ Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  rev_implies:  Q bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A
Lemmas referenced :  fpf_ap_pair_lemma istype-void istype-universe assert_wf fpf-dom_wf subtype-fpf2 top_wf subtype_rel_wf deq_wf fpf_wf append_wf filter_wf5 l_member_wf bnot_wf deq-member_wf member_append member_filter eqtt_to_assert assert-deq-member eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin sqequalRule cut introduction extract_by_obid dependent_functionElimination isect_memberEquality_alt voidElimination hypothesis functionIsType isectElimination hypothesisEquality universeIsType applyEquality lambdaEquality_alt inhabitedIsType independent_isectElimination lambdaFormation_alt because_Cache universeEquality isect_memberFormation_alt axiomEquality equalityTransitivity equalitySymmetry dependent_pairEquality_alt setElimination rename setIsType independent_functionElimination unionElimination inlFormation_alt productIsType inrFormation_alt equalityElimination dependent_set_memberEquality_alt dependent_pairFormation_alt equalityIsType1 promote_hyp instantiate cumulativity

\mforall{}[A:Type].  \mforall{}[B,C,D:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[g:a:A  fp->  C[a]].  \mforall{}[eq:EqDecider(A)].
    (f  \moplus{}  g  \mmember{}  a:A  fp->  D[a])  supposing 
          ((\mforall{}a:A.  ((\muparrow{}a  \mmember{}  dom(g))  {}\mRightarrow{}  (C[a]  \msubseteq{}r  D[a])))  and 
          (\mforall{}a:A.  ((\muparrow{}a  \mmember{}  dom(f))  {}\mRightarrow{}  (B[a]  \msubseteq{}r  D[a]))))

Date html generated: 2019_10_16-AM-11_25_19
Last ObjectModification: 2018_10_10-PM-01_24_35

Theory : finite!partial!functions

Home Index