---

Step * of Lemma face_lattice-1-join-irreducible

∀I:fset(ℕ). ∀x,y:Point(face_lattice(I)).
  (x ∨ y = 1 ∈ Point(face_lattice(I)) ⇐⇒ (x = 1 ∈ Point(face_lattice(I))) ∨ (y = 1 ∈ Point(face_lattice(I))))
BY
{ ((UnivCD THENA Auto) THEN All (Unfold `face_lattice`) THEN RWO "face-lattice-1-join-irreducible" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:fset(\mBbbN{}).  \mforall{}x,y:Point(face\_lattice(I)).    (x  \mvee{}  y  =  1  \mLeftarrow{}{}\mRightarrow{}  (x  =  1)  \mvee{}  (y  =  1))


By

---

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

---

Home Index