---

Step * of Lemma case-real3-req2

∀[f:ℕ+ ⟶ 𝔹]. ∀[b:ℝ]. ∀[a:Top].  (case-real3(a;b;f) = b) supposing ∀n:ℕ+. (¬↑(f n))
BY
{ (Intros
   THEN Unfold `case-real3` 0
   THEN Subst' case-real3-seq(a;b;f) = b ∈ ℝ 0
   THEN Auto
   THEN Symmetry
   THEN EqTypeCD
   THEN Auto) }

1
1. f : ℕ+ ⟶ 𝔹
2. ∀n:ℕ+. (¬↑(f n))
3. b : ℝ
4. a : Top
⊢ b = case-real3-seq(a;b;f) ∈ (ℕ+ ⟶ ℤ)

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[b:\mBbbR{}].  \mforall{}[a:Top].    (case-real3(a;b;f)  =  b)  supposing  \mforall{}n:\mBbbN{}\msupplus{}.  (\mneg{}\muparrow{}(f  n))


By

---

Latex:
(Intros
  THEN  Unfold  `case-real3`  0
  THEN  Subst'  case-real3-seq(a;b;f)  =  b  0
  THEN  Auto
  THEN  Symmetry
  THEN  EqTypeCD
  THEN  Auto)

---

Home Index