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