---

Step * 1 of Lemma dec_iff_ex_bvfun


1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(E x y)
⊢ ∃f:T ⟶ T ⟶ 𝔹. ∀x,y:T.  (↑(f x y) ⇐⇒ E x y)
BY
{ (((RenameVar `g' 3 THENM Unfold `decidable` 3)
   THENM (With ⌜λx,y. case g x y of inl(a) => tt | inr(b) => ff⌝ (D 0) THENA Auto)
   )
THENM Reduce 0
) }

1
1. [T] : Type
2. [E] : T ⟶ T ⟶ ℙ
3. g : ∀x,y:T.  ((E x y) ∨ (¬(E x y)))@i
⊢ ∀x,y:T.  (↑case g x y of inl(a) => tt | inr(b) => ff ⇐⇒ E x y)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [E]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x,y:T.    Dec(E  x  y)
\mvdash{}  \mexists{}f:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:T.    (\muparrow{}(f  x  y)  \mLeftarrow{}{}\mRightarrow{}  E  x  y)


By

---

Latex:
(((RenameVar  `g'  3  THENM  Unfold  `decidable`  3)
  THENM  (With  \mkleeneopen{}\mlambda{}x,y.  case  g  x  y  of  inl(a)  =>  tt  |  inr(b)  =>  ff\mkleeneclose{}  (D  0)  THENA  Auto)
  )
THENM  Reduce  0
)

---

Home Index