---

Step * of Lemma weak-continuity-principle-nat-nat

∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f:ℕ ⟶ ℕ. ∀G:n:ℕ ⟶ {g:ℕ ⟶ ℕ| f = g ∈ (ℕn ⟶ ℕ)} .  ∃n:ℕ. ((F f) = (F (G n)) ∈ ℕ)
BY
{ (InstLemma `weak-continuity-nat-nat` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN Assert ⌜↓∃n:ℕ. ((F f) = (F (G n)) ∈ ℕ)⌝⋅) }

1
.....assertion..... 
1. F : (ℕ ⟶ ℕ) ⟶ ℕ
2. f : ℕ ⟶ ℕ
3. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
4. G : n:ℕ ⟶ {g:ℕ ⟶ ℕ| f = g ∈ (ℕn ⟶ ℕ)} 
⊢ ↓∃n:ℕ. ((F f) = (F (G n)) ∈ ℕ)

2
1. F : (ℕ ⟶ ℕ) ⟶ ℕ
2. f : ℕ ⟶ ℕ
3. ⇃(∃n:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕn ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ)))
4. G : n:ℕ ⟶ {g:ℕ ⟶ ℕ| f = g ∈ (ℕn ⟶ ℕ)} 
5. ↓∃n:ℕ. ((F f) = (F (G n)) ∈ ℕ)
⊢ ∃n:ℕ. ((F f) = (F (G n)) ∈ ℕ)

---

Latex:

---

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}G:n:\mBbbN{}  {}\mrightarrow{}  \{g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}|  f  =  g\}  .    \mexists{}n:\mBbbN{}.  ((F  f)  =  (F  (G  n)))


By

---

Latex:
(InstLemma  `weak-continuity-nat-nat`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  Assert  \mkleeneopen{}\mdownarrow{}\mexists{}n:\mBbbN{}.  ((F  f)  =  (F  (G  n)))\mkleeneclose{}\mcdot{})

---

Home Index