---

Step * of Lemma face-lattice-le-1

∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).  (x ≤ y ⇐⇒ fset-ac-le(union-deq(T;T;eq;eq);x;y))
BY
{ (Intros
   THEN (InstLemma `free-dlwc-le` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;⌜λ2x.face-lattice-constraints(x)⌝;⌜x⌝;⌜y⌝]⋅
         THENA Auto
         )
   THEN RepUR ``face-lattice`` 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}x,y:Point(face-lattice(T;eq)).
    (x  \mleq{}  y  \mLeftarrow{}{}\mRightarrow{}  fset-ac-le(union-deq(T;T;eq;eq);x;y))


By

---

Latex:
(Intros
  THEN  (InstLemma  `free-dlwc-le`  [\mkleeneopen{}T  +  T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.face-lattice-constraints(x)\mkleeneclose{};
              \mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RepUR  ``face-lattice``  0
  THEN  Trivial)

---

Home Index