---

Step * of Lemma cubical-term-restriction-is-1

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[I:fset(ℕ)]. ∀[rho:Gamma(I)]. ∀[J:fset(ℕ)]. ∀[f:J ⟶ I].
  ((phi(rho) = 1 ∈ Point(face_lattice(I))) ⇒ (phi(f(rho)) = 1 ∈ Point(face_lattice(J))))
BY
{ (Auto THEN (RWW  "cubical-term-at-morph< -1" 0 THENA Auto) THEN RWW "face-type-ap-morph" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[rho:Gamma(I)].  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].
    ((phi(rho)  =  1)  {}\mRightarrow{}  (phi(f(rho))  =  1))


By

---

Latex:
(Auto
  THEN  (RWW    "cubical-term-at-morph<  -1"  0  THENA  Auto)
  THEN  RWW  "face-type-ap-morph"  0
  THEN  Auto)

---

Home Index