---

Step * of Lemma face-lattice-1-join-irreducible

∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)).
  (x ∨ y = 1 ∈ Point(face-lattice(T;eq)) ⇐⇒ (x = 1 ∈ Point(face-lattice(T;eq))) ∨ (y = 1 ∈ Point(face-lattice(T;eq))))
BY
{ ((UnivCD THENA Auto) THEN All (Unfold `face-lattice`) THEN RWO "free-dlwc-1-join-irreducible" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}x,y:Point(face-lattice(T;eq)).    (x  \mvee{}  y  =  1  \mLeftarrow{}{}\mRightarrow{}  (x  =  1)  \mvee{}  (y  =  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  All  (Unfold  `face-lattice`)
  THEN  RWO  "free-dlwc-1-join-irreducible"  0
  THEN  Auto)

---

Home Index