---

Step * of Lemma face-or-eq-1

No Annotations
∀[Gamma:j⊢]
  ∀r,s:{Gamma ⊢ _:𝔽}. ∀I:fset(ℕ). ∀rho:Gamma(I).
    ((r ∨ s)(rho) = 1 ∈ Point(face_lattice(I))
    ⇐⇒ (r(rho) = 1 ∈ Point(face_lattice(I))) ∨ (s(rho) = 1 ∈ Point(face_lattice(I))))
BY
{ ((UnivCD THENA Auto) THEN (RWO "face-or-at" 0 THENA Auto) THEN RWO "face_lattice-1-join-irreducible" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}]
    \mforall{}r,s:\{Gamma  \mvdash{}  \_:\mBbbF{}\}.  \mforall{}I:fset(\mBbbN{}).  \mforall{}rho:Gamma(I).    ((r  \mvee{}  s)(rho)  =  1  \mLeftarrow{}{}\mRightarrow{}  (r(rho)  =  1)  \mvee{}  (s(rho)  =  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "face-or-at"  0  THENA  Auto)
  THEN  RWO  "face\_lattice-1-join-irreducible"  0
  THEN  Auto)

---

Home Index