Nuprl Lemma : subtype_rel_quotient

[A,B:Type]. ∀[E:B ⟶ B ⟶ ℙ].  ((x,y:A//E[x;y]) ⊆(x,y:B//E[x;y])) supposing (EquivRel(B;x,y.E[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] 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] prop: implies:  Q quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] guard: {T}
Lemmas referenced :  quotient_wf equiv_rel_subtype equiv_rel_wf subtype_rel_wf quotient-member-eq equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality sqequalRule applyEquality hypothesis because_Cache independent_isectElimination universeEquality independent_functionElimination axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality pointwiseFunctionalityForEquality pertypeElimination productElimination dependent_functionElimination productEquality

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

Date html generated: 2016_05_14-AM-06_08_05
Last ObjectModification: 2015_12_26-AM-11_48_32

Theory : quot_1

Home Index