Step
*
of Lemma
ax_choice
∀[A,B:Type]. ∀[Q:A ⟶ B ⟶ ℙ]. ((∀x:A. ∃y:B. Q[x;y])
⇒ (∃f:A ⟶ B. ∀x:A. Q[x;f x]))
BY
{ Auto }
1
1. [A] : Type
2. [B] : Type
3. [Q] : A ⟶ B ⟶ ℙ
4. ∀x:A. ∃y:B. Q[x;y]
⊢ ∃f:A ⟶ B. ∀x:A. Q[x;f x]
Latex:
Latex:
\mforall{}[A,B:Type]. \mforall{}[Q:A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}]. ((\mforall{}x:A. \mexists{}y:B. Q[x;y]) {}\mRightarrow{} (\mexists{}f:A {}\mrightarrow{} B. \mforall{}x:A. Q[x;f x]))
By
Latex:
Auto
Home
Index