### Nuprl Lemma : disjoint-quotient_subtype

`∀[A,B:Type].`
`  ∀[E:(A + B) ⟶ (A + B) ⟶ ℙ]`
`    (x,y:A + B//E[x;y]) ⊆r (a1,a2:A//E[inl a1;inl a2] + (b1,b2:B//E[inr b1 ;inr b2 ])) `
`    supposing EquivRel(A + B;x,y.E[x;y]) `
`  supposing ¬(A ∧ B)`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` not: `¬A` and: `P ∧ Q` function: `x:A ⟶ B[x]` inr: `inr x ` inl: `inl x` union: `left + right` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` sym: `Sym(T;x,y.E[x; y])` implies: `P `` Q` prop: `ℙ` so_apply: `x[s1;s2]` trans: `Trans(T;x,y.E[x; y])` subtype_rel: `A ⊆r B` so_lambda: `λ2x y.t[x; y]` quotient: `x,y:A//B[x; y]` guard: `{T}` not: `¬A` cand: `A c∧ B` false: `False`
Lemmas referenced :  quotient_wf quotient-member-eq equal_wf equal-wf-base equiv_rel_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution independent_pairFormation productElimination thin promote_hyp lambdaFormation hypothesisEquality applyEquality functionExtensionality unionEquality cumulativity inlEquality inrEquality lambdaEquality pointwiseFunctionalityForEquality extract_by_obid isectElimination sqequalRule independent_isectElimination hypothesis pertypeElimination equalityTransitivity equalitySymmetry because_Cache rename unionElimination dependent_functionElimination independent_functionElimination productEquality universeEquality axiomEquality isect_memberEquality functionEquality voidElimination

Latex:
\mforall{}[A,B:Type].
\mforall{}[E:(A  +  B)  {}\mrightarrow{}  (A  +  B)  {}\mrightarrow{}  \mBbbP{}]
(x,y:A  +  B//E[x;y])  \msubseteq{}r  (a1,a2:A//E[inl  a1;inl  a2]  +  (b1,b2:B//E[inr  b1  ;inr  b2  ]))
supposing  EquivRel(A  +  B;x,y.E[x;y])
supposing  \mneg{}(A  \mwedge{}  B)

Date html generated: 2017_04_14-AM-07_39_55
Last ObjectModification: 2017_02_27-PM-03_11_18

Theory : quot_1

Home Index