---

Step * of Lemma face_lattice-le

∀[I:fset(ℕ)]. ∀[x,y:Point(face_lattice(I))].
  uiff(x ≤ y;∀f:I ⟶ I. (((x)<f> = 1 ∈ Point(face_lattice(I))) ⇒ ((y)<f> = 1 ∈ Point(face_lattice(I)))))
BY
{ Auto }

1
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))

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))))
⊢ x ≤ y

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x,y:Point(face\_lattice(I))].    uiff(x  \mleq{}  y;\mforall{}f:I  {}\mrightarrow{}  I.  (((x)<f>  =  1)  {}\mRightarrow{}  ((y)<f>  =  1)))


By

---

Latex:
Auto

---

Home Index