---

Step * of Lemma gamma-neighbourhood-prop1

∀beta:ℕ ⟶ ℕ. ∀n0:finite-nat-seq().
  ((∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x))))
  ∧ (∀a,b:finite-nat-seq().
       ((↑isl(gamma-neighbourhood(beta;n0) a))
       ⇒ ((gamma-neighbourhood(beta;n0) a) = (gamma-neighbourhood(beta;n0) a**b) ∈ (ℕ?)))))
BY
{ Auto }

1
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. a : ℕ ⟶ ℕ
⊢ ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x)))

2
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. ∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x)))
4. a : finite-nat-seq()
5. b : finite-nat-seq()
6. ↑isl(gamma-neighbourhood(beta;n0) a)
⊢ (gamma-neighbourhood(beta;n0) a) = (gamma-neighbourhood(beta;n0) a**b) ∈ (ℕ?)

---

Latex:

---

Latex:
\mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n0:finite-nat-seq().
    ((\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}x:\mBbbN{}.  (\muparrow{}isl(gamma-neighbourhood(beta;n0)  a\^{}(x))))
    \mwedge{}  (\mforall{}a,b:finite-nat-seq().
              ((\muparrow{}isl(gamma-neighbourhood(beta;n0)  a))
              {}\mRightarrow{}  ((gamma-neighbourhood(beta;n0)  a)  =  (gamma-neighbourhood(beta;n0)  a**b)))))


By

---

Latex:
Auto

---

Home Index