Nuprl Lemma : stable-implies-sq_stable
∀[A:ℙ]. (Stable{A} ⇒ SqStable(A))
Proof
Definitions occuring in Statement :
sq_stable: SqStable(P),
stable: Stable{P},
uall: ∀[x:A]. B[x],
prop: ℙ,
implies: P ⇒ Q
Definitions unfolded in proof :
or: P ∨ Q,
false: False,
squash: ↓T,
not: ¬A,
uimplies: b supposing a,
stable: Stable{P},
prop: ℙ,
member: t ∈ T,
sq_stable: SqStable(P),
implies: P ⇒ Q,
uall: ∀[x:A]. B[x]
Lemmas referenced :
minimal-not-not-excluded-middle,
minimal-double-negation-hyp-elim,
not_wf,
or_wf,
false_wf,
stable_wf,
squash_wf
Rules used in proof :
unionElimination,
voidElimination,
independent_functionElimination,
imageElimination,
independent_isectElimination,
because_Cache,
functionEquality,
universeEquality,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[A:\mBbbP{}]. (Stable\{A\} {}\mRightarrow{} SqStable(A))
Date html generated:
2017_09_29-PM-05_47_24
Last ObjectModification:
2017_08_04-PM-05_29_53
Theory : call!by!value_2
Home
Index