---

Step * of Lemma dM-to-FL-sq

∀[I,J,v:Top].  (dM-to-FL(I;v) ~ dM-to-FL(J;v))
BY
{ ((UnivCD THENA Auto)
   THEN (RepUR ``dM-to-FL lattice-extend lattice-fset-join lattice-join lattice-0 lattice-1`` 0
         THEN RepUR ``lattice-fset-meet lattice-meet union-deq`` 0
         )
   THEN EqCD) }

1
1. I : Top
2. J : Top
3. v : Top
⊢ λx,y. (face_lattice(I)."join" x y) ~ λx,y. (face_lattice(J)."join" x y)

2
1. I : Top
2. J : Top
3. v : Top
⊢ face_lattice(I)."0" ~ face_lattice(J)."0"

3
1. I : Top
2. J : Top
3. v : Top
⊢ λxs.reduce(λx,y. (face_lattice(I)."meet" x y);1;λx.case x of inl(a) => (a=1) | inr(a) => (a=0)"(xs))"(v) 
~ λxs.reduce(λx,y. (face_lattice(J)."meet" x y);1;λx.case x of inl(a) => (a=1) | inr(a) => (a=0)"(xs))"(v)

---

Latex:

---

Latex:
\mforall{}[I,J,v:Top].    (dM-to-FL(I;v)  \msim{}  dM-to-FL(J;v))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RepUR  ``dM-to-FL  lattice-extend  lattice-fset-join  lattice-join  lattice-0  lattice-1``  0
              THEN  RepUR  ``lattice-fset-meet  lattice-meet  union-deq``  0
              )
  THEN  EqCD)

---

Home Index