---

Step * of Lemma es-interface-from-decidable

∀[Info:Type]. ∀[A:es:EO+(Info) ⟶ e:E ⟶ Type]. ∀[R:es:EO+(Info) ⟶ e:E ⟶ A[es;e] ⟶ ℙ].
  ((∀es:EO+(Info). ∀e:E.  Dec(∃a:A[es;e]. R[es;e;a]))
  ⇒ (∃X:EClass(A[es;e]). ∀es:EO+(Info). ∀e:E.  ((↑e ∈b X ⇐⇒ ∃a:A[es;e]. R[es;e;a]) ∧ R[es;e;X(e)] supposing ↑e ∈b X)))
BY
{ Auto }

1
1. [Info] : Type
2. [A] : es:EO+(Info) ⟶ e:E ⟶ Type
3. [R] : es:EO+(Info) ⟶ e:E ⟶ A[es;e] ⟶ ℙ
4. ∀es:EO+(Info). ∀e:E.  Dec(∃a:A[es;e]. R[es;e;a])@i'
⊢ ∃X:EClass(A[es;e]). ∀es:EO+(Info). ∀e:E.  ((↑e ∈b X ⇐⇒ ∃a:A[es;e]. R[es;e;a]) ∧ R[es;e;X(e)] supposing ↑e ∈b X)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[A:es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  Type].  \mforall{}[R:es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  A[es;e]  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(\mexists{}a:A[es;e].  R[es;e;a]))
    {}\mRightarrow{}  (\mexists{}X:EClass(A[es;e])
              \mforall{}es:EO+(Info).  \mforall{}e:E.
                  ((\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A[es;e].  R[es;e;a])  \mwedge{}  R[es;e;X(e)]  supposing  \muparrow{}e  \mmember{}\msubb{}  X)))


By

---

Latex:
Auto

---

Home Index