---

Step * 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 ∈ ℤ)))
⊢ False
BY
{ (InstHyp [⌜λi.if i <z k then 0 else 1 fi ⌝;⌜k⌝] (-1)⋅ THEN Auto) }

1
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...}. (((λi.if i <z k then 0 else 1 fi ) m) = 0 ∈ ℤ)
⊢ False

---

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)))
\mvdash{}  False


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}i.if  i  <z  k  then  0  else  1  fi  \mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index