---

Step * of Lemma implies-nh-comp-satisfies

∀[I,J,K:fset(ℕ)]. ∀[psi:Point(face_lattice(I))]. ∀[f:J ⟶ I]. ∀[g:K ⟶ J].  (psi f ⋅ g) = 1 supposing (psi f) = 1
BY
{ (Auto THEN ParallelLast) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. K : fset(ℕ)
4. psi : Point(face_lattice(I))
5. f : J ⟶ I
6. g : K ⟶ J
7. (psi)<f> = 1 ∈ Point(face_lattice(J))
⊢ (psi)<f ⋅ g> = 1 ∈ Point(face_lattice(K))

---

Latex:

---

Latex:
\mforall{}[I,J,K:fset(\mBbbN{})].  \mforall{}[psi:Point(face\_lattice(I))].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[g:K  {}\mrightarrow{}  J].
    (psi  f  \mcdot{}  g)  =  1  supposing  (psi  f)  =  1


By

---

Latex:
(Auto  THEN  ParallelLast)

---

Home Index