Nuprl Lemma : quotient_subtype_quotient

[A,B:Type]. ∀[EA:A ⟶ A ⟶ ℙ]. ∀[EB:B ⟶ B ⟶ ℙ].
  ((x,y:A//EA[x;y]) ⊆(x,y:B//EB[x;y])) supposing 
     ((∀x,y:A.  (EA[x;y]  EB[x;y])) and 
     EquivRel(A;x,y.EA[x;y]) and 
     EquivRel(B;x,y.EB[x;y]) and 
     (A ⊆B))


Definitions occuring in Statement :  equiv_rel: EquivRel(T;x,y.E[x; y]) quotient: x,y:A//B[x; y] uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] guard: {T} implies:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  quotient_wf quotient-member-eq equal-wf-base subtype_rel_self all_wf equiv_rel_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality pointwiseFunctionalityForEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule applyEquality independent_isectElimination hypothesis pertypeElimination productElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination productEquality because_Cache instantiate axiomEquality functionEquality isect_memberEquality cumulativity universeEquality

\mforall{}[A,B:Type].  \mforall{}[EA:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[EB:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    ((x,y:A//EA[x;y])  \msubseteq{}r  (x,y:B//EB[x;y]))  supposing 
          ((\mforall{}x,y:A.    (EA[x;y]  {}\mRightarrow{}  EB[x;y]))  and 
          EquivRel(A;x,y.EA[x;y])  and 
          EquivRel(B;x,y.EB[x;y])  and 
          (A  \msubseteq{}r  B))

Date html generated: 2018_05_21-PM-00_04_41
Last ObjectModification: 2018_05_11-AM-10_50_13

Theory : quot_1

Home Index