Step * of Lemma face-term-0-and-1

No Annotations
G:j⊢G.𝕀 ⊢ (((q=0) ∧ (q=1))  0(𝔽))
BY
(Auto THEN THEN Auto) }

1
1. CubicalSet{j}
2. fset(ℕ)
3. rho G.𝕀(I)
4. ((q=0) ∧ (q=1))(rho) 1 ∈ Point(face_lattice(I))
⊢ 0(𝔽)(rho) 1 ∈ Point(face_lattice(I))

2
.....wf..... 
1. CubicalSet{j}
2. fset(ℕ)
3. rho G.𝕀(I)
⊢ ((q=0) ∧ (q=1))(rho) ∈ Point(face_lattice(I))


Latex:


Latex:
No  Annotations
\mforall{}G:j\mvdash{}.  G.\mBbbI{}  \mvdash{}  (((q=0)  \mwedge{}  (q=1))  {}\mRightarrow{}  0(\mBbbF{}))


By


Latex:
(Auto  THEN  D  0  THEN  Auto)




Home Index