---

Step * of Lemma basic-continuity

∀[F:(ℤ ⟶ ℤ) ⟶ ℤ]. ∀[f:ℤ ⟶ ℤ].
  (↓∃n:ℕ. ∀[g:ℤ ⟶ ℤ]. (F f) = (F g) ∈ ℤ supposing ∀[i:ℤ]. (f i) = (g i) ∈ ℤ supposing |i| < n)
BY
{ Intros }

1
1. [F] : (ℤ ⟶ ℤ) ⟶ ℤ
2. [f] : ℤ ⟶ ℤ
⊢ ↓∃n:ℕ. ∀[g:ℤ ⟶ ℤ]. (F f) = (F g) ∈ ℤ supposing ∀[i:ℤ]. (f i) = (g i) ∈ ℤ supposing |i| < n

---

Latex:

---

Latex:
\mforall{}[F:(\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}].
    (\mdownarrow{}\mexists{}n:\mBbbN{}.  \mforall{}[g:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}].  (F  f)  =  (F  g)  supposing  \mforall{}[i:\mBbbZ{}].  (f  i)  =  (g  i)  supposing  |i|  <  n)


By

---

Latex:
Intros

---

Home Index