---

Step * of Lemma face-and-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-and-at" 0 THENA Auto) THEN RWO "lattice-meet-eq-1" 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  \mwedge{}  s)(rho)  =  1  \mLeftarrow{}{}\mRightarrow{}  (r(rho)  =  1)  \mwedge{}  (s(rho)  =  1))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "face-and-at"  0  THENA  Auto)  THEN  RWO  "lattice-meet-eq-1"  0  THEN  Auto)

---

Home Index