Nuprl Lemma : partial-not-exception
∀[T:Type]. ∀[x:partial(T)]. (¬is-exception(x))
Proof
Definitions occuring in Statement :
partial: partial(T),
is-exception: is-exception(t),
uall: ∀[x:A]. B[x],
not: ¬A,
universe: Type
Definitions unfolded in proof :
prop: ℙ,
and: P ∧ Q,
quotient: x,y:A//B[x; y],
partial: partial(T),
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
squash: ↓T,
is-exception: is-exception(t),
rev_implies: P ⇐ Q,
false: False,
not: ¬A,
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
true: True
Lemmas referenced :
is-exception_wf,
base-partial-not-exception,
not_wf,
squash_wf,
true_wf,
equal-wf-base,
base-partial_wf,
per-partial_wf,
partial_wf
Rules used in proof :
universeEquality,
cumulativity,
because_Cache,
hypothesisEquality,
isectElimination,
lemma_by_obid,
productEquality,
hypothesis,
thin,
productElimination,
cut,
pertypeElimination,
sqequalRule,
pointwiseFunctionalityForEquality,
sqequalHypSubstitution,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
baseClosed,
imageMemberEquality,
equalitySymmetry,
equalityTransitivity,
imageElimination,
lambdaEquality,
applyEquality,
sqleExtensionalEquality,
voidElimination,
independent_functionElimination,
lambdaFormation,
independent_pairFormation,
natural_numberEquality
Latex:
\mforall{}[T:Type]. \mforall{}[x:partial(T)]. (\mneg{}is-exception(x))
Date html generated:
2019_06_20-PM-00_33_43
Last ObjectModification:
2018_10_15-PM-09_42_01
Theory : partial_1
Home
Index