---

Step * 1 of Lemma fl_all-implies-instance


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))))
BY
{ (BLemma`face_lattice-induction`  THEN Auto) }

1
1. I : fset(ℕ)
2. x : Point(dM(I))
3. i : ℕ
4. v : Point(face_lattice(I+i))
5. y : Point(face_lattice(I+i))
6. ((∀i.v) = 1 ∈ Point(face_lattice(I))) ⇒ ((v)<(i/x)> = 1 ∈ Point(face_lattice(I)))
7. ((∀i.y) = 1 ∈ Point(face_lattice(I))) ⇒ ((y)<(i/x)> = 1 ∈ Point(face_lattice(I)))
8. (∀i.v ∨ y) = 1 ∈ Point(face_lattice(I))
⊢ (v ∨ y)<(i/x)> = 1 ∈ Point(face_lattice(I))

2
1. I : fset(ℕ)
2. x : Point(dM(I))
3. i : ℕ
4. v : Point(face_lattice(I+i))
5. ((∀i.v) = 1 ∈ Point(face_lattice(I))) ⇒ ((v)<(i/x)> = 1 ∈ Point(face_lattice(I)))
6. i1 : names(I+i)
7. (∀i.(i1=0) ∧ v) = 1 ∈ Point(face_lattice(I))
⊢ ((i1=0) ∧ v)<(i/x)> = 1 ∈ Point(face_lattice(I))

3
1. I : fset(ℕ)
2. x : Point(dM(I))
3. i : ℕ
4. v : Point(face_lattice(I+i))
5. ((∀i.v) = 1 ∈ Point(face_lattice(I))) ⇒ ((v)<(i/x)> = 1 ∈ Point(face_lattice(I)))
6. i1 : names(I+i)
7. ((∀i.(i1=0) ∧ v) = 1 ∈ Point(face_lattice(I))) ⇒ (((i1=0) ∧ v)<(i/x)> = 1 ∈ Point(face_lattice(I)))
8. (∀i.(i1=1) ∧ v) = 1 ∈ Point(face_lattice(I))
⊢ ((i1=1) ∧ v)<(i/x)> = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma`face\_lattice-induction`    THEN  Auto)

---

Home Index