---

Step * 1 of Lemma full-partition-non-dec


1. I : Interval
2. icompact(I)
3. p : partition(I)
⊢ sorted-by(λx,y. (x ≤ y);p @ [right-endpoint(I)])
BY
{ (BLemma `sorted-by-append`
   THEN Auto
   THEN Try ((BLemma `sorted-by-single` THEN Auto)⋅)
   THEN Try (((BLemma `frs-non-dec-sorted-by` THENA Auto) THEN D (-1) THEN Unhide THEN Auto))
   THEN Reduce 0
   THEN RWW "l_all_single l_all_iff" 0
   THEN Auto) }

1
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. sorted-by(λx,y. (x ≤ y);p)
5. sorted-by(λx,y. (x ≤ y);[right-endpoint(I)])
6. a : ℝ
7. (a ∈ p)
⊢ a ≤ right-endpoint(I)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  p  :  partition(I)
\mvdash{}  sorted-by(\mlambda{}x,y.  (x  \mleq{}  y);p  @  [right-endpoint(I)])


By

---

Latex:
(BLemma  `sorted-by-append`
  THEN  Auto
  THEN  Try  ((BLemma  `sorted-by-single`  THEN  Auto)\mcdot{})
  THEN  Try  (((BLemma  `frs-non-dec-sorted-by`  THENA  Auto)  THEN  D  (-1)  THEN  Unhide  THEN  Auto))
  THEN  Reduce  0
  THEN  RWW  "l\_all\_single  l\_all\_iff"  0
  THEN  Auto)

---

Home Index