---

Step * of Lemma face-or-list-eq-1

No Annotations
∀[Gamma:j⊢]
  ∀L:{Gamma ⊢ _:𝔽} List. ∀I:fset(ℕ). ∀rho:Gamma(I).
    (\/(L)(rho) = 1 ∈ Point(face_lattice(I)) ⇐⇒ (∃x∈L. x(rho) = 1 ∈ Point(face_lattice(I))))
BY
{ (InductionOnList THEN (UnivCD THENA Auto)) }

1
1. [Gamma] : CubicalSet{j}
2. I : fset(ℕ)
3. rho : Gamma(I)
⊢ \/([])(rho) = 1 ∈ Point(face_lattice(I)) ⇐⇒ (∃x∈[]. x(rho) = 1 ∈ Point(face_lattice(I)))

2
1. [Gamma] : CubicalSet{j}
2. u : {Gamma ⊢ _:𝔽}
3. v : {Gamma ⊢ _:𝔽} List
4. ∀I:fset(ℕ). ∀rho:Gamma(I).  (\/(v)(rho) = 1 ∈ Point(face_lattice(I)) ⇐⇒ (∃x∈v. x(rho) = 1 ∈ Point(face_lattice(I))))
5. I : fset(ℕ)
6. rho : Gamma(I)
⊢ \/([u / v])(rho) = 1 ∈ Point(face_lattice(I)) ⇐⇒ (∃x∈[u / v]. x(rho) = 1 ∈ Point(face_lattice(I)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}]
    \mforall{}L:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  List.  \mforall{}I:fset(\mBbbN{}).  \mforall{}rho:Gamma(I).    (\mbackslash{}/(L)(rho)  =  1  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}x\mmember{}L.  x(rho)  =  1))


By

---

Latex:
(InductionOnList  THEN  (UnivCD  THENA  Auto))

---

Home Index