---

Step * of Lemma case-real2_wf2

∀[d,a,b:ℝ]. ∀[f:a ≠ b ⟶ ((↓r0 < d) ∨ (↓¬(r0 < d)))].
  (case-real2(a;b;f) ∈ {z:ℝ| ((r0 < d) ⇒ (z = a)) ∧ ((d ≤ r0) ⇒ (z = b))} )
BY
{ (Intros
   THEN (InstLemma `case-real2_wf` [⌜r0 < d⌝;⌜a⌝;⌜b⌝;⌜f⌝]⋅ THENA Auto)
   THEN DoSubsume
   THEN Try (Trivial)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[d,a,b:\mBbbR{}].  \mforall{}[f:a  \mneq{}  b  {}\mrightarrow{}  ((\mdownarrow{}r0  <  d)  \mvee{}  (\mdownarrow{}\mneg{}(r0  <  d)))].
    (case-real2(a;b;f)  \mmember{}  \{z:\mBbbR{}|  ((r0  <  d)  {}\mRightarrow{}  (z  =  a))  \mwedge{}  ((d  \mleq{}  r0)  {}\mRightarrow{}  (z  =  b))\}  )


By

---

Latex:
(Intros
  THEN  (InstLemma  `case-real2\_wf`  [\mkleeneopen{}r0  <  d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DoSubsume
  THEN  Try  (Trivial)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index