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