---

Step * 2 of Lemma face_lattice-le


1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
4. ∀f:I ⟶ I. (((x)<f> = 1 ∈ Point(face_lattice(I))) ⇒ ((y)<f> = 1 ∈ Point(face_lattice(I))))
⊢ x ≤ y
BY
{ (Unfold `face_lattice` 0 THEN BLemma `face-lattice-le` THEN Auto) }

1
1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
4. ∀f:I ⟶ I. (((x)<f> = 1 ∈ Point(face_lattice(I))) ⇒ ((y)<f> = 1 ∈ Point(face_lattice(I))))
5. s : fset(names(I) + names(I))
6. s ∈ x
⊢ ↓∃t:fset(names(I) + names(I)). (t ∈ y ∧ t ⊆ s)

2
1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
4. ∀f:I ⟶ I. (((x)<f> = 1 ∈ Point(face_lattice(I))) ⇒ ((y)<f> = 1 ∈ Point(face_lattice(I))))
5. s : fset(names(I) + names(I))
⊢ x ∈ fset(fset(names(I) + names(I)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  Point(face\_lattice(I))
3.  y  :  Point(face\_lattice(I))
4.  \mforall{}f:I  {}\mrightarrow{}  I.  (((x)<f>  =  1)  {}\mRightarrow{}  ((y)<f>  =  1))
\mvdash{}  x  \mleq{}  y


By

---

Latex:
(Unfold  `face\_lattice`  0  THEN  BLemma  `face-lattice-le`  THEN  Auto)

---

Home Index