---

Step * of Lemma fl_all-implies-instance

∀[I:fset(ℕ)]. ∀[x:Point(dM(I))]. ∀[i:ℕ]. ∀[v:Point(face_lattice(I+i))].
  (((∀i.v) = 1 ∈ Point(face_lattice(I))) ⇒ ((v)<(i/x)> = 1 ∈ Point(face_lattice(I))))
BY
{ (Intros THEN RepeatFor 2 (MoveToConcl (-1))) }

1
1. I : fset(ℕ)
2. x : Point(dM(I))
3. i : ℕ
⊢ ∀v:Point(face_lattice(I+i)). (((∀i.v) = 1 ∈ Point(face_lattice(I))) ⇒ ((v)<(i/x)> = 1 ∈ Point(face_lattice(I))))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:Point(dM(I))].  \mforall{}[i:\mBbbN{}].  \mforall{}[v:Point(face\_lattice(I+i))].
    (((\mforall{}i.v)  =  1)  {}\mRightarrow{}  ((v)<(i/x)>  =  1))


By

---

Latex:
(Intros  THEN  RepeatFor  2  (MoveToConcl  (-1)))

---

Home Index