---

Step * of Lemma case-real3_wf

∀[f:ℕ+ ⟶ 𝔹]. ∀[b:ℝ]. ∀[a:ℝ supposing ∃n:ℕ+. (↑(f n))].
  case-real3(a;b;f) ∈ ℝ supposing ∀n,m:ℕ+.  ((↑(f n)) ⇒ (¬↑(f m)) ⇒ (|(a m) - b m| ≤ 4))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[b:\mBbbR{}].  \mforall{}[a:\mBbbR{}  supposing  \mexists{}n:\mBbbN{}\msupplus{}.  (\muparrow{}(f  n))].
    case-real3(a;b;f)  \mmember{}  \mBbbR{}  supposing  \mforall{}n,m:\mBbbN{}\msupplus{}.    ((\muparrow{}(f  n))  {}\mRightarrow{}  (\mneg{}\muparrow{}(f  m))  {}\mRightarrow{}  (|(a  m)  -  b  m|  \mleq{}  4))


By

---

Latex:
ProveWfLemma

---

Home Index