---

Step * of Lemma rmin-stable-cases

∀a,b:ℝ. ∀P:Type.  (Stable{P} ⇒ (((rmin(a;b) = a) ⇒ P) ∧ ((rmin(a;b) = b) ⇒ P)) ⇒ P)
BY
{ (Auto
   THEN (StableCases ⌜rmin(a;b) = a⌝⋅ THEN Auto)
   THEN StableCases ⌜rmin(a;b) = b⌝⋅
   THEN Auto
   THEN InstLemma `rmin-classical-cases` [⌜a⌝;⌜b⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.  \mforall{}P:Type.    (Stable\{P\}  {}\mRightarrow{}  (((rmin(a;b)  =  a)  {}\mRightarrow{}  P)  \mwedge{}  ((rmin(a;b)  =  b)  {}\mRightarrow{}  P))  {}\mRightarrow{}  P)


By

---

Latex:
(Auto
  THEN  (StableCases  \mkleeneopen{}rmin(a;b)  =  a\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  StableCases  \mkleeneopen{}rmin(a;b)  =  b\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  InstLemma  `rmin-classical-cases`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index