---

Step * of Lemma finite-cantor-decider_wf

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀dcdr:∀x,y:T.  Dec(R[x;y]). ∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T.
    (finite-cantor-decider(dcdr;n;F) ∈ Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g]))
BY
{ Auto }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. dcdr : ∀x,y:T.  Dec(R[x;y])
4. n : ℕ
5. F : (ℕn ⟶ 𝔹) ⟶ T
⊢ finite-cantor-decider(dcdr;n;F) ∈ Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}dcdr:\mforall{}x,y:T.    Dec(R[x;y]).  \mforall{}n:\mBbbN{}.  \mforall{}F:(\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.
        (finite-cantor-decider(dcdr;n;F)  \mmember{}  Dec(\mexists{}f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  R[F  f;F  g]))


By

---

Latex:
Auto

---

Home Index