---

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


1. ∀t:{t:ℝ| t ∈ [r(-1), r1]} . ((↓t ∈ [r(-1), r0]) ∨ (↓t ∈ [r0, r1]))
2. x : ℝ
3. r(-1) < x
4. x < r1
⊢ (r0 ≤ x) ∨ (x ≤ r0)
BY
{ ((D 1 With ⌜x⌝  THENA Auto) THEN (D -1 THENL [OrRight; OrLeft]) THEN Auto) }

1
1. x : ℝ
2. r(-1) < x
3. x < r1
4. ↓x ∈ [r(-1), r0]
⊢ x ≤ r0

2
1. x : ℝ
2. r(-1) < x
3. x < r1
4. ↓x ∈ [r0, r1]
⊢ r0 ≤ x

---

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{}
3.  r(-1)  <  x
4.  x  <  r1
\mvdash{}  (r0  \mleq{}  x)  \mvee{}  (x  \mleq{}  r0)


By

---

Latex:
((D  1  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)  THEN  (D  -1  THENL  [OrRight;  OrLeft])  THEN  Auto)

---

Home Index