---

Step * 2 of Lemma exists_det_fun


1. [T] : Type
2. [A] : T ⟶ ℙ
3. ∀x:T. SqStable(A x)@i
4. ∀x:T. Dec(A x)@i
⊢ detach_fun(T;A)
BY
{ (RepUR ``all decidable or`` -1 THEN RenameVar `g' (-1) THEN With ⌜λx.isl(g x)⌝ (D 0)⋅ THEN Auto) }

1
1. T : Type
2. A : T ⟶ ℙ
3. ∀x:T. SqStable(A x)@i
4. g : x:T ⟶ (A x + (¬(A x)))@i
5. x : T@i
6. A x@i
⊢ ↑isl(g x)

2
1. T : Type
2. A : T ⟶ ℙ
3. ∀x:T. SqStable(A x)@i
4. g : x:T ⟶ (A x + (¬(A x)))@i
5. x : T@i
6. ↑((λx.isl(g x)) x)@i
⊢ A x

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  SqStable(A  x)@i
4.  \mforall{}x:T.  Dec(A  x)@i
\mvdash{}  detach\_fun(T;A)


By

---

Latex:
(RepUR  ``all  decidable  or``  -1  THEN  RenameVar  `g'  (-1)  THEN  With  \mkleeneopen{}\mlambda{}x.isl(g  x)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index