Nuprl Lemma : decidable-subtype

[P,Q:ℙ].  (Dec(P) ⊆Dec(Q)) supposing ((Q  P) and (P ⊆Q))


Definitions occuring in Statement :  decidable: Dec(P) uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] prop: implies:  Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a decidable: Dec(P) subtype_rel: A ⊆B or: P ∨ Q prop: implies:  Q squash: T
Lemmas referenced :  subtype_rel_wf or_wf subtype_rel_not not_wf subtype_rel_union
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality sqequalHypSubstitution hypothesisEquality applyEquality lemma_by_obid isectElimination thin hypothesis independent_isectElimination lambdaFormation independent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination because_Cache axiomEquality functionEquality isect_memberEquality equalityTransitivity equalitySymmetry universeEquality

\mforall{}[P,Q:\mBbbP{}].    (Dec(P)  \msubseteq{}r  Dec(Q))  supposing  ((Q  {}\mRightarrow{}  P)  and  (P  \msubseteq{}r  Q))

Date html generated: 2016_05_13-PM-03_19_47
Last ObjectModification: 2016_01_14-PM-04_34_13

Theory : subtype_0

Home Index