Step
*
1
1
1
1
of Lemma
gen-continuity-is-false
1. ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ∀f:ℕ ⟶ ℕ. ((P f)
⇒ ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ))
⇒ (P g))))
2. ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((0s = g ∈ (ℕk ⟶ ℕ))
⇒ ((λf.∀n:ℕ. ∃m:{n...}. ((f m) = 0 ∈ ℤ)) g)))
3. k : ℕ
4. ∀g:ℕ ⟶ ℕ. ((0s = g ∈ (ℕk ⟶ ℕ))
⇒ (∀n:ℕ. ∃m:{n...}. ((g m) = 0 ∈ ℤ)))
5. m : {k...}
6. if m <z k then 0 else 1 fi = 0 ∈ ℤ
⊢ False
BY
{ (SplitOnHypITE -1 THEN Auto) }
Latex:
Latex:
1. \mforall{}P:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbP{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((P f) {}\mRightarrow{} \00D9(\mexists{}k:\mBbbN{}. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((f = g) {}\mRightarrow{} (P g))))
2. \00D9(\mexists{}k:\mBbbN{}. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((0s = g) {}\mRightarrow{} ((\mlambda{}f.\mforall{}n:\mBbbN{}. \mexists{}m:\{n...\}. ((f m) = 0)) g)))
3. k : \mBbbN{}
4. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((0s = g) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. \mexists{}m:\{n...\}. ((g m) = 0)))
5. m : \{k...\}
6. if m <z k then 0 else 1 fi = 0
\mvdash{} False
By
Latex:
(SplitOnHypITE -1 THEN Auto)
Home
Index