### Nuprl Lemma : decidable-subtype

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

Proof

Definitions occuring in Statement :  decidable: `Dec(P)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` decidable: `Dec(P)` subtype_rel: `A ⊆r B` or: `P ∨ Q` prop: `ℙ` implies: `P `` 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

Latex:
\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