Nuprl Lemma : decidable__per-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/per/E[x;y].  Dec(u = v ∈ (x,y:T/per/E[x;y]))))
Proof
Definitions occuring in Statement : 
per-quotient: x,y:T/per/E[x; y]
, 
equiv_rel: EquivRel(T;x,y.E[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 : 
per-quotient: x,y:T/per/E[x; y]
, 
quotient: x,y:A//B[x; y]
Lemmas referenced : 
decidable__quotient_equal
Rules used in proof : 
cut, 
introduction, 
extract_by_obid, 
sqequalRule, 
sqequalReflexivity, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
hypothesis
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/per/E[x;y].    Dec(u  =  v)))
Date html generated:
2019_06_20-PM-00_33_33
Last ObjectModification:
2018_08_21-PM-10_54_15
Theory : per-quotient
Home
Index