---

Step * 2 1 of Lemma context-subset-is-cubical-subset


1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
⊢ (λI@0,J,f,rho. f(rho))
= (λU,U',f,ux. ux ⋅ f)
∈ (x:fset(ℕ)
  ⟶ y:fset(ℕ)
  ⟶ y ⟶ x
  ⟶ {rho:formal-cube(I)(x)| phi(rho) = 1 ∈ Point(face_lattice(x))} 
  ⟶ {rho:formal-cube(I)(y)| phi(rho) = 1 ∈ Point(face_lattice(y))} )
BY
{ RepeatFor 4 (((FunExt THEN Reduce 0) THENA Auto)) }

1
1. I : fset(ℕ)
2. phi : {formal-cube(I) ⊢ _:𝔽}
3. x : fset(ℕ)
4. y : fset(ℕ)
5. x1 : y ⟶ x
6. x2 : {rho:formal-cube(I)(x)| phi(rho) = 1 ∈ Point(face_lattice(x))} 
⊢ x1(x2) = x2 ⋅ x1 ∈ {rho:formal-cube(I)(y)| phi(rho) = 1 ∈ Point(face_lattice(y))} 

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  phi  :  \{formal-cube(I)  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  (\mlambda{}I@0,J,f,rho.  f(rho))  =  (\mlambda{}U,U',f,ux.  ux  \mcdot{}  f)


By

---

Latex:
RepeatFor  4  (((FunExt  THEN  Reduce  0)  THENA  Auto))

---

Home Index