---

Step * of Lemma partition-refines_transitivity

∀I:Interval. ∀P,Q,R:partition(I).  (P refines Q ⇒ Q refines R ⇒ P refines R) supposing icompact(I)
BY
{ (Unfold `partition-refines` 0 THEN Auto THEN FLemma `frs-refines_transitivity` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}P,Q,R:partition(I).    (P  refines  Q  {}\mRightarrow{}  Q  refines  R  {}\mRightarrow{}  P  refines  R)  supposing  icompact(I)


By

---

Latex:
(Unfold  `partition-refines`  0  THEN  Auto  THEN  FLemma  `frs-refines\_transitivity`  [-1;-2]  THEN  Auto)

---

Home Index