---

Step * of Lemma separated-partitions-have-common-refinement

∀I:Interval
  ∀P,Q:partition(I).
    (separated-partitions(P;Q) ⇒ (∃R:partition(I). (frs-increasing(R) ∧ frs-refines(R;P) ∧ frs-refines(R;Q)))) 
  supposing icompact(I)
BY
{ xxx(Auto
      THEN InstLemma `frs-increasing-separated-common-refinement` [⌜P⌝;⌜Q⌝]⋅
      THEN Auto
      THEN ParallelLast
      THEN Auto
      THEN MemTypeCD
      THEN Auto
      THEN D 0
      THEN Try ((BLemma `frs-increasing-non-dec` THEN Auto)))xxx }

1
1. I : Interval
2. icompact(I)
3. P : partition(I)
4. Q : partition(I)
5. separated-partitions(P;Q)
6. r : ℝ List
7. frs-increasing(r)
8. frs-refines(r;P)
9. frs-refines(r;Q)
10. frs-refines(P @ Q;r)
⊢ 0 < ||r|| ⇒ ((left-endpoint(I) ≤ r[0]) ∧ (last(r) ≤ right-endpoint(I)))

---

Latex:

---

Latex:
\mforall{}I:Interval
    \mforall{}P,Q:partition(I).
        (separated-partitions(P;Q)
        {}\mRightarrow{}  (\mexists{}R:partition(I).  (frs-increasing(R)  \mwedge{}  frs-refines(R;P)  \mwedge{}  frs-refines(R;Q)))) 
    supposing  icompact(I)


By

---

Latex:
xxx(Auto
        THEN  InstLemma  `frs-increasing-separated-common-refinement`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{}]\mcdot{}
        THEN  Auto
        THEN  ParallelLast
        THEN  Auto
        THEN  MemTypeCD
        THEN  Auto
        THEN  D  0
        THEN  Try  ((BLemma  `frs-increasing-non-dec`  THEN  Auto)))xxx

---

Home Index