---

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

¬(∀t:{t:ℝ| t ∈ [r(-1), r1]} . ((↓t ∈ [r(-1), r0]) ∨ (↓t ∈ [r0, r1])))
BY
{ (InstLemma `not-all-nonneg-or-nonpos` [] THEN ParallelLast THEN Auto) }

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

---

Latex:

---

Latex:
\mneg{}(\mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [r(-1),  r1]\}  .  ((\mdownarrow{}t  \mmember{}  [r(-1),  r0])  \mvee{}  (\mdownarrow{}t  \mmember{}  [r0,  r1])))


By

---

Latex:
(InstLemma  `not-all-nonneg-or-nonpos`  []  THEN  ParallelLast  THEN  Auto)

---

Home Index