---

Step * of Lemma gamma-neighbourhood-prop3

∀beta:ℕ ⟶ ℕ. ∀n,m:ℕ.
  (((beta 0) = 0 ∈ ℤ)
  ⇒ (↑isl(gamma-neighbourhood(beta;0s^(n)) 0s^(m)))
  ⇒ (n < m ∧ ((gamma-neighbourhood(beta;0s^(n)) 0s^(m)) = (inl 0) ∈ (ℕ?))))
BY
{ (UnivCD THENA Auto) }

1
1. beta : ℕ ⟶ ℕ
2. n : ℕ
3. m : ℕ
4. (beta 0) = 0 ∈ ℤ
5. ↑isl(gamma-neighbourhood(beta;0s^(n)) 0s^(m))
⊢ n < m ∧ ((gamma-neighbourhood(beta;0s^(n)) 0s^(m)) = (inl 0) ∈ (ℕ?))

---

Latex:

---

Latex:
\mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n,m:\mBbbN{}.
    (((beta  0)  =  0)
    {}\mRightarrow{}  (\muparrow{}isl(gamma-neighbourhood(beta;0s\^{}(n))  0s\^{}(m)))
    {}\mRightarrow{}  (n  <  m  \mwedge{}  ((gamma-neighbourhood(beta;0s\^{}(n))  0s\^{}(m))  =  (inl  0))))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index