---

Step * 1 of Lemma partition-refines_weakening


1. I : Interval
2. [%] : icompact(I)
3. P : partition(I)
4. Q : partition(I)
5. P = Q ∈ partition(I)
⊢ Q refines Q
BY
{ (Unfold `partition-refines` 0 THEN BLemma `frs-refines_weakening` THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  [\%]  :  icompact(I)
3.  P  :  partition(I)
4.  Q  :  partition(I)
5.  P  =  Q
\mvdash{}  Q  refines  Q


By

---

Latex:
(Unfold  `partition-refines`  0  THEN  BLemma  `frs-refines\_weakening`  THEN  Auto)

---

Home Index