---

Step * of Lemma gamma-neighbourhood-prop5

∀beta:ℕ ⟶ ℕ. ∀n,m:ℕ.
  ((¬((beta 0) = 0 ∈ ℤ))
  ⇒ (↑isl(gamma-neighbourhood(beta;0s^(n)) 0s^(m)))
  ⇒ (n < m ∧ ((gamma-neighbourhood(beta;0s^(n)) 0s^(m)) = (inl 1) ∈ (ℕ?))))
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 1) ∈ (ℕ?))

---

Latex:

---

Latex:
\mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n,m:\mBbbN{}.
    ((\mneg{}((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  1))))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index