---

Step * 1 of Lemma union-of-intervals-not-interval


1. ∀t:{t:ℝ| t ∈ [r(-1), r1]} . ((↓t ∈ [r(-1), r0]) ∨ (↓t ∈ [r0, r1]))
2. x : ℝ
⊢ (r0 ≤ x) ∨ (x ≤ r0)
BY
{ ((InstLemma `rless-cases` [⌜r(-1)⌝;⌜r0⌝;⌜x⌝]⋅ THENA Auto) THEN D -1 THEN Auto) }

1
1. ∀t:{t:ℝ| t ∈ [r(-1), r1]} . ((↓t ∈ [r(-1), r0]) ∨ (↓t ∈ [r0, r1]))
2. x : ℝ
3. r(-1) < x
⊢ (r0 ≤ x) ∨ (x ≤ r0)

---

Latex:

---

Latex:

1.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r(-1),  r1]\}  .  ((\mdownarrow{}t  \mmember{}  [r(-1),  r0])  \mvee{}  (\mdownarrow{}t  \mmember{}  [r0,  r1]))
2.  x  :  \mBbbR{}
\mvdash{}  (r0  \mleq{}  x)  \mvee{}  (x  \mleq{}  r0)


By

---

Latex:
((InstLemma  `rless-cases`  [\mkleeneopen{}r(-1)\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index