---

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

∀F:(ℕ+ ⟶ ℤ) ⟶ ℕ. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} .  ∃n:ℕ+. ((F f) = (F (G n)) ∈ ℕ)
BY
{ ((Auto THEN (InstLemma `weak-continuity-nat-int`  [⌜λf.(F (λn.(f (n - 1))))⌝;λn.(f (n + 1))]⋅ THENA Auto))
   THEN Reduce -1
   THEN Assert ⌜↓∃n:ℕ. ((F f) = (F (G (n + 1))) ∈ ℕ)⌝⋅) }

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

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

---

Latex:

---

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


By

---

Latex:
((Auto
    THEN  (InstLemma  `weak-continuity-nat-int`    [\mkleeneopen{}\mlambda{}f.(F  (\mlambda{}n.(f  (n  -  1))))\mkleeneclose{};\mlambda{}n.(f  (n  +  1))]\mcdot{}  THENA  Auto)
    )
  THEN  Reduce  -1
  THEN  Assert  \mkleeneopen{}\mdownarrow{}\mexists{}n:\mBbbN{}.  ((F  f)  =  (F  (G  (n  +  1))))\mkleeneclose{}\mcdot{})

---

Home Index