Nuprl Lemma : allowed-trivial-iff
∀[T:𝕌']. ∀[x:Provisional(T)]. ∀[X:ℙ]. (SqStable(X) ⇒ allowed(x) ⇐⇒ usquash(allowed(x) ∧ X) supposing X)
Proof
Definitions occuring in Statement :
allowed: allowed(x),
provisional-type: Provisional(T),
usquash: usquash(T),
sq_stable: SqStable(P),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
uimplies: b supposing a,
iff: P ⇐⇒ Q,
and: P ∧ Q,
member: t ∈ T,
prop: ℙ,
rev_implies: P ⇐ Q,
cand: A c∧ B,
squash: ↓T
Lemmas referenced :
allowed_wf,
usquash_wf,
sq_stable_wf,
provisional-type_wf,
istype-universe,
squash-implies-usquash,
usquash-elim,
sq_stable__and,
sq_stable__allowed
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
independent_pairFormation,
universeIsType,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
productEquality,
universeEquality,
instantiate,
independent_functionElimination,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination,
isect_memberEquality_alt,
because_Cache,
productElimination
Latex:
\mforall{}[T:\mBbbU{}']. \mforall{}[x:Provisional(T)]. \mforall{}[X:\mBbbP{}].
(SqStable(X) {}\mRightarrow{} allowed(x) \mLeftarrow{}{}\mRightarrow{} usquash(allowed(x) \mwedge{} X) supposing X)
Date html generated:
2020_05_20-AM-08_00_55
Last ObjectModification:
2020_05_17-PM-06_33_02
Theory : monads
Home
Index