Nuprl Lemma : strong-subtype-set1

[A:Type]. ∀[P,Q:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;{x:A| Q[x]} supposing ∀x:A. (P[x]  Q[x])


Proof




Definitions occuring in Statement :  strong-subtype: strong-subtype(A;B) uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B prop: implies:  Q
Lemmas referenced :  strong-subtype-set strong-subtype-self strong-subtype_witness all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache independent_isectElimination hypothesis sqequalRule lambdaEquality applyEquality setEquality universeEquality independent_functionElimination functionEquality isect_memberEquality equalityTransitivity equalitySymmetry cumulativity

Latex:
\mforall{}[A:Type].  \mforall{}[P,Q:A  {}\mrightarrow{}  \mBbbP{}].    strong-subtype(\{x:A|  P[x]\}  ;\{x:A|  Q[x]\}  )  supposing  \mforall{}x:A.  (P[x]  {}\mRightarrow{}  Q[x])



Date html generated: 2016_05_13-PM-04_11_13
Last ObjectModification: 2015_12_26-AM-11_21_27

Theory : subtype_1


Home Index