---

Step * of Lemma avoid-reals

∀L:ℝ List. ∀a,b:ℝ.  ((a < b) ⇒ (∃a',b':ℝ. ((a ≤ a') ∧ (b' ≤ b) ∧ (a' < b') ∧ (∀x∈L.(x < a') ∨ (b' < x)))))
BY
{ (InductionOnList
   THEN Auto
   THEN (InstHyp [⌜a⌝;⌜b⌝] 3⋅ THENA Auto)
   THEN ExRepD
   THEN (InstLemma `avoid-real` [⌜a'⌝;⌜b'⌝;⌜u⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto
   THEN RWO "l_all_cons" 0
   THEN Auto) }

1
1. u : ℝ
2. v : ℝ List
3. ∀a,b:ℝ.  ((a < b) ⇒ (∃a',b':ℝ. ((a ≤ a') ∧ (b' ≤ b) ∧ (a' < b') ∧ (∀x∈v.(x < a') ∨ (b' < x)))))
4. a : ℝ
5. b : ℝ
6. a < b
7. a' : ℝ
8. b' : ℝ
9. a ≤ a'
10. b' ≤ b
11. a' < b'
12. (∀x∈v.(x < a') ∨ (b' < x))
13. a'@0 : ℝ
14. b'@0 : ℝ
15. a' ≤ a'@0
16. b'@0 ≤ b'
17. a'@0 < b'@0
18. (u < a'@0) ∨ (b'@0 < u)
19. a ≤ a'@0
20. b'@0 ≤ b
21. a'@0 < b'@0
22. (u < a'@0) ∨ (b'@0 < u)
⊢ (∀x∈v.(x < a'@0) ∨ (b'@0 < x))

---

Latex:

---

Latex:
\mforall{}L:\mBbbR{}  List.  \mforall{}a,b:\mBbbR{}.
    ((a  <  b)  {}\mRightarrow{}  (\mexists{}a',b':\mBbbR{}.  ((a  \mleq{}  a')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  (a'  <  b')  \mwedge{}  (\mforall{}x\mmember{}L.(x  <  a')  \mvee{}  (b'  <  x)))))


By

---

Latex:
(InductionOnList
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstLemma  `avoid-real`  [\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  RWO  "l\_all\_cons"  0
  THEN  Auto)

---

Home Index