Step
*
1
of Lemma
notAC20-ssq
1. T : Type
2. ↓T
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃m:T. (P n m)))
⇒ (↓∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))
⊢ False
BY
{ (InstLemma `not-choice-baire-to-nat-ssq` [] THEN D (-1) THEN RepeatFor 3 ((D 0 THENA Auto))) }
1
1. T : Type
2. ↓T
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃m:T. (P n m)))
⇒ (↓∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))
4. P : ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ
5. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t])
⊢ ↓∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]
2
1. T : Type
2. ↓T
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (↓∃m:T. (P n m)))
⇒ (↓∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))
4. P : ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ
5. ↓∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t]
⊢ ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t])
Latex:
Latex:
1. T : Type
2. \mdownarrow{}T
3. \mforall{}P:((\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
((\mforall{}n:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. (\mdownarrow{}\mexists{}m:T. (P n m)))
{}\mRightarrow{} (\mdownarrow{}\mexists{}f:((\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} T. \mforall{}n:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. (P n (f n))))
\mvdash{} False
By
Latex:
(InstLemma `not-choice-baire-to-nat-ssq` [] THEN D (-1) THEN RepeatFor 3 ((D 0 THENA Auto)))
Home
Index