---

Step * of Lemma extract-decider-of-decidable-prop

∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∀t:T. ((P t) ∨ (¬(P t)))) ⇒ (∃f:T ⟶ 𝔹. ∀t:T. (↑(f t) ⇐⇒ P t)))
BY
{ Auto }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀t:T. ((P t) ∨ (¬(P t)))@i
⊢ ∃f:T ⟶ 𝔹. ∀t:T. (↑(f t) ⇐⇒ P t)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}t:T.  ((P  t)  \mvee{}  (\mneg{}(P  t))))  {}\mRightarrow{}  (\mexists{}f:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}t:T.  (\muparrow{}(f  t)  \mLeftarrow{}{}\mRightarrow{}  P  t)))


By

---

Latex:
Auto

---

Home Index