Nuprl Lemma : fpf-compatible-wf2

`∀[A:Type]. ∀[B,C:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]].`
`  f || g ∈ ℙ supposing ∀x:A. ((↑x ∈ dom(f)) `` (↑x ∈ dom(g)) `` (B[x] ⊆r C[x]))`

Proof

Definitions occuring in Statement :  fpf-compatible: `f || g` 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]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  fpf-compatible: `f || g` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` and: `P ∧ Q` subtype_rel: `A ⊆r B` so_apply: `x[s]` all: `∀x:A. B[x]` top: `Top`
Lemmas referenced :  all_wf assert_wf fpf-dom_wf subtype-fpf2 top_wf equal_wf fpf-ap_wf subtype_rel_wf fpf_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality lambdaEquality functionEquality productEquality because_Cache applyEquality functionExtensionality hypothesis independent_isectElimination lambdaFormation isect_memberEquality voidElimination voidEquality productElimination dependent_functionElimination independent_functionElimination axiomEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\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]].
f  ||  g  \mmember{}  \mBbbP{}  supposing  \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(f))  {}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(g))  {}\mRightarrow{}  (B[x]  \msubseteq{}r  C[x]))

Date html generated: 2018_05_21-PM-09_19_55
Last ObjectModification: 2018_02_09-AM-10_17_47

Theory : finite!partial!functions

Home Index