---

Step * of Lemma full-partition-non-dec

∀[I:Interval]. ∀[p:partition(I)]. frs-non-dec(full-partition(I;p)) supposing icompact(I)
BY
{ (Auto
   THEN Unfold `full-partition` 0
   THEN (BLemma `frs-non-dec-sorted-by` THENA Auto)
   THEN BLemma `sorted-by-cons`
   THEN Auto
   THEN Reduce 0) }

1
1. I : Interval
2. icompact(I)
3. p : partition(I)
⊢ sorted-by(λx,y. (x ≤ y);p @ [right-endpoint(I)])

2
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. sorted-by(λx,y. (x ≤ y);p @ [right-endpoint(I)])
⊢ (∀z∈p @ [right-endpoint(I)].left-endpoint(I) ≤ z)

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[p:partition(I)].  frs-non-dec(full-partition(I;p))  supposing  icompact(I)


By

---

Latex:
(Auto
  THEN  Unfold  `full-partition`  0
  THEN  (BLemma  `frs-non-dec-sorted-by`  THENA  Auto)
  THEN  BLemma  `sorted-by-cons`
  THEN  Auto
  THEN  Reduce  0)

---

Home Index