### Nuprl Lemma : decidable__quotient_equal

`∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].`
`  (EquivRel(T;x,y.E[x;y]) `` (∀x,y:T.  Dec(E[x;y])) `` (∀u,v:x,y:T//E[x;y].  Dec(u = v ∈ (x,y:T//E[x;y]))))`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` so_apply: `x[s1;s2]` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` exists: `∃x:A. B[x]` quotient: `x,y:A//B[x; y]` subtype_rel: `A ⊆r B` infix_ap: `x f y` trans: `Trans(T;x,y.E[x; y])` equiv_rel: `EquivRel(T;x,y.E[x; y])` guard: `{T}` sym: `Sym(T;x,y.E[x; y])` sq_stable: `SqStable(P)` squash: `↓T`
Lemmas referenced :  istype-universe decidable_wf equiv_rel_wf dec_iff_ex_bvfun quotient_wf equal_wf bool_wf subtype_rel_self iff_imp_equal_bool assert_wf assert_witness sq_stable__iff sq_stable_from_decidable decidable__assert sq_stable__equal squash_wf iff_wf infix_ap_wf quot_elim subtype_quotient
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  sqequalRule Error :functionIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis Error :inhabitedIsType,  Error :universeIsType,  applyEquality Error :lambdaEquality_alt,  universeEquality cumulativity functionExtensionality because_Cache independent_isectElimination productElimination independent_functionElimination Error :functionExtensionality_alt,  pointwiseFunctionalityForEquality functionEquality pertypeElimination equalityTransitivity equalitySymmetry rename instantiate Error :equalityIsType1,  dependent_functionElimination Error :productIsType,  Error :equalityIsType4,  independent_pairFormation promote_hyp Error :dependent_pairFormation_alt,  independent_pairEquality axiomEquality Error :functionIsTypeImplies,  imageElimination imageMemberEquality baseClosed

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(EquivRel(T;x,y.E[x;y])  {}\mRightarrow{}  (\mforall{}x,y:T.    Dec(E[x;y]))  {}\mRightarrow{}  (\mforall{}u,v:x,y:T//E[x;y].    Dec(u  =  v)))

Date html generated: 2019_06_20-PM-00_32_18
Last ObjectModification: 2018_10_05-PM-05_44_32

Theory : quot_1

Home Index