---

Step * of Lemma poset-cat-dist-flip

∀I:Cname List. ∀x:cat-ob(poset-cat(I)). ∀a:nameset(I).  (((x a) = 0 ∈ ℤ) ⇒ (1 ≤ poset-cat-dist(I;x;flip(x;a))))
BY
{ (Auto
   THEN RepUR ``poset-cat-dist`` 0
   THEN (Assert I ∈ nameset(I) List BY
               (Unfold `nameset` 0 THEN Auto))
   THEN (Assert 0 < ||filter(λi.((x i =z 0) ∧b (flip(x;a) i =z 1));I)|| BY
               BLemma `length-filter-pos`)
   THEN Auto) }

1
1. I : Cname List
2. x : cat-ob(poset-cat(I))
3. a : nameset(I)
4. (x a) = 0 ∈ ℤ
5. I ∈ nameset(I) List
⊢ (∃x1∈I. ↑((λi.((x i =z 0) ∧b (flip(x;a) i =z 1))) x1))

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}x:cat-ob(poset-cat(I)).  \mforall{}a:nameset(I).
    (((x  a)  =  0)  {}\mRightarrow{}  (1  \mleq{}  poset-cat-dist(I;x;flip(x;a))))


By

---

Latex:
(Auto
  THEN  RepUR  ``poset-cat-dist``  0
  THEN  (Assert  I  \mmember{}  nameset(I)  List  BY
                          (Unfold  `nameset`  0  THEN  Auto))
  THEN  (Assert  0  <  ||filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (flip(x;a)  i  =\msubz{}  1));I)||  BY
                          BLemma  `length-filter-pos`)
  THEN  Auto)

---

Home Index