### Nuprl Lemma : fpf-sub_witness

`∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]].  (f ⊆ g `` (λx,y. <Ax, Ax> ∈ f ⊆ g))`

Proof

Definitions occuring in Statement :  fpf-sub: `f ⊆ g` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` implies: `P `` Q` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` pair: `<a, b>` universe: `Type` axiom: `Ax`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` fpf-sub: `f ⊆ g` all: `∀x:A. B[x]` cand: `A c∧ B` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` top: `Top` prop: `ℙ` guard: `{T}`
Lemmas referenced :  assert_witness fpf-dom_wf subtype-fpf2 top_wf assert_wf fpf-sub_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule lambdaEquality independent_pairEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis independent_isectElimination isect_memberEquality voidElimination voidEquality because_Cache independent_functionElimination axiomEquality cumulativity dependent_functionElimination equalityTransitivity equalitySymmetry productElimination

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:a:A  fp->  B[a]].    (f  \msubseteq{}  g  {}\mRightarrow{}  (\mlambda{}x,y.  <Ax,  Ax>  \mmember{}  f  \000C\msubseteq{}  g))

Date html generated: 2018_05_21-PM-09_18_41
Last ObjectModification: 2018_02_09-AM-10_17_15

Theory : finite!partial!functions

Home Index