---

Step * of Lemma poset-cat-arrow-iff

∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].  uiff(cat-arrow(poset-cat(I)) x y;{∀i:nameset(I). ((x i) ≤ (y i))})
BY
{ (RepUR ``cat-arrow cat-ob poset-cat guard`` 0
   THEN Auto
   THEN (InstHyp [⌜i⌝] (-2)⋅ THEN Auto)
   THEN RW assert_pushdownC (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x,y:cat-ob(poset-cat(I))].
    uiff(cat-arrow(poset-cat(I))  x  y;\{\mforall{}i:nameset(I).  ((x  i)  \mleq{}  (y  i))\})


By

---

Latex:
(RepUR  ``cat-arrow  cat-ob  poset-cat  guard``  0
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto)

---

Home Index