---

Step * of Lemma poset-cat-dist-add

∀[I:Cname List]. ∀[x,y,z:cat-ob(poset-cat(I))].
  (poset-cat-dist(I;x;z) = (poset-cat-dist(I;x;y) + poset-cat-dist(I;y;z)) ∈ ℤ) supposing 
     ((cat-arrow(poset-cat(I)) x y) and 
     (cat-arrow(poset-cat(I)) y z))
BY
{ (Auto THEN Unfold `poset-cat-dist` 0 THEN All (RepUR ``cat-ob cat-arrow poset-cat``)) }

1
1. I : Cname List
2. x : name-morph(I;[])
3. y : name-morph(I;[])
4. z : name-morph(I;[])
5. ∀x:nameset(I). (↑y x ≤z z x)
6. ∀x@0:nameset(I). (↑x x@0 ≤z y x@0)
⊢ ||filter(λi.((x i =z 0) ∧b (z i =z 1));I)||
= (||filter(λi.((x i =z 0) ∧b (y i =z 1));I)|| + ||filter(λi.((y i =z 0) ∧b (z i =z 1));I)||)
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x,y,z:cat-ob(poset-cat(I))].
    (poset-cat-dist(I;x;z)  =  (poset-cat-dist(I;x;y)  +  poset-cat-dist(I;y;z)))  supposing 
          ((cat-arrow(poset-cat(I))  x  y)  and 
          (cat-arrow(poset-cat(I))  y  z))


By

---

Latex:
(Auto  THEN  Unfold  `poset-cat-dist`  0  THEN  All  (RepUR  ``cat-ob  cat-arrow  poset-cat``))

---

Home Index