---

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

∀F:(ℕ ⟶ ℤ) ⟶ ℕ. ∀f:ℕ ⟶ ℤ. ∀G:n:ℕ ⟶ {g:ℕ ⟶ ℤ| f = g ∈ (ℕn ⟶ ℤ)} .  ∃n:ℕ. ((F f) = (F (G n)) ∈ ℕ)
BY
{ (InstLemma `weak-continuity-nat-int` []
   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{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}G:n:\mBbbN{}  {}\mrightarrow{}  \{g:\mBbbN{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\}  .    \mexists{}n:\mBbbN{}.  ((F  f)  =  (F  (G  n)))


By

---

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

---

Home Index