---

Step * 1 of Lemma face_lattice-le


1. I : fset(ℕ)
2. x : Point(face_lattice(I))
3. y : Point(face_lattice(I))
4. x ≤ y
5. f : I ⟶ I
6. (x)<f> = 1 ∈ Point(face_lattice(I))
⊢ (y)<f> = 1 ∈ Point(face_lattice(I))
BY
{ ((Assert (x)<f> ≤ (y)<f> BY
          (BLemma `lattice-hom-le` THEN Auto))
   THEN (RWO  "-2" (-1) THENA Auto)
   THEN RWO "lattice-1-le-iff" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  (x)<f>  \mleq{}  (y)<f>  BY
                (BLemma  `lattice-hom-le`  THEN  Auto))
  THEN  (RWO    "-2"  (-1)  THENA  Auto)
  THEN  RWO  "lattice-1-le-iff"  (-1)
  THEN  Auto)

---

Home Index