Nuprl Lemma : is-above-inl

[A,B:Type]. ∀[a:A].  ∀z:Base. (is-above(A B;inl a;z)  (∃c:Base. ((z inl c) ∧ is-above(A;a;c))))


Proof




Definitions occuring in Statement :  is-above: is-above(T;a;z) uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q inl: inl x union: left right base: Base universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q exists: x:A. B[x] member: t ∈ T is-above: is-above(T;a;z) and: P ∧ Q assert: b ifthenelse: if then else fi  isl: isl(x) btrue: tt true: True prop: outl: outl(x) bfalse: ff false: False cand: c∧ B uimplies: supposing a has-value: (a)↓ or: P ∨ Q not: ¬A
Lemmas referenced :  assert_wf isl_wf true_wf false_wf equal_wf is-above_wf base_wf has-value-monotonic has-value_wf_base is-exception_wf has-value-implies-dec-isinl-2 equal-wf-base-T sqle_wf_base not-btrue-sqle-bfalse
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation dependent_pairFormation sqequalRule baseApply closedConclusion baseClosed hypothesisEquality sqequalHypSubstitution productElimination thin cut hypothesis natural_numberEquality hyp_replacement equalitySymmetry applyLambdaEquality introduction extract_by_obid isectElimination cumulativity equalityTransitivity unionEquality unionElimination voidElimination dependent_functionElimination independent_functionElimination sqequalIntensionalEquality productEquality inlEquality universeEquality independent_pairFormation independent_isectElimination divergentSqle sqleReflexivity because_Cache promote_hyp sqleRule

Latex:
\mforall{}[A,B:Type].  \mforall{}[a:A].
    \mforall{}z:Base.  (is-above(A  +  B;inl  a;z)  {}\mRightarrow{}  (\mexists{}c:Base.  ((z  \msim{}  inl  c)  \mwedge{}  is-above(A;a;c))))



Date html generated: 2017_04_14-AM-07_37_09
Last ObjectModification: 2017_02_27-PM-03_09_22

Theory : subtype_1


Home Index