Step
*
9
of Lemma
quot_ring_sig
.....subterm..... T:t
2:n
1. r : CRng
2. a : |r| ⟶ ℙ
3. a Ideal of r
4. ∀x:|r|. SqStable(a x)
5. d : |r| ⟶ 𝔹
6. ∀x:|r|. (a x
⇐⇒ ↑(d x))
7. Carrier(r/d) ∈ Type
⊢ λx,y. (inr ⋅ ) ∈ Carrier(r/d) ⟶ Carrier(r/d) ⟶ (Carrier(r/d)?)
BY
{ Auto }
Latex:
Latex:
.....subterm..... T:t
2:n
1. r : CRng
2. a : |r| {}\mrightarrow{} \mBbbP{}
3. a Ideal of r
4. \mforall{}x:|r|. SqStable(a x)
5. d : |r| {}\mrightarrow{} \mBbbB{}
6. \mforall{}x:|r|. (a x \mLeftarrow{}{}\mRightarrow{} \muparrow{}(d x))
7. Carrier(r/d) \mmember{} Type
\mvdash{} \mlambda{}x,y. (inr \mcdot{} ) \mmember{} Carrier(r/d) {}\mrightarrow{} Carrier(r/d) {}\mrightarrow{} (Carrier(r/d)?)
By
Latex:
Auto
Home
Index