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: P ⇒ Q,
and: P ∧ Q,
inl: inl x,
union: left + right,
base: Base,
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
member: t ∈ T,
is-above: is-above(T;a;z),
and: P ∧ Q,
assert: ↑b,
ifthenelse: if b then t else f fi ,
isl: isl(x),
btrue: tt,
true: True,
prop: ℙ,
outl: outl(x),
bfalse: ff,
false: False,
cand: A c∧ B,
uimplies: b 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