---

Step * 1 of Lemma face-lattice-subset-le


1. T : Type@i'
2. eq : EqDecider(T)@i
3. x : Point(face-lattice(T;eq))@i
4. y : Point(face-lattice(T;eq))@i
5. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
6. x ⊆ y@i
7. s : fset(T + T)@i
8. s ∈ x@i
⊢ ↓∃t:fset(T + T). (t ∈ y ∧ t ⊆ s)
BY
{ ((D 0 THEN D 0 With ⌜s⌝ ) THEN Auto) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. x : Point(face-lattice(T;eq))@i
4. y : Point(face-lattice(T;eq))@i
5. Point(face-lattice(T;eq)) ⊆r fset(fset(T + T))
6. x ⊆ y@i
7. s : fset(T + T)@i
8. s ∈ x@i
9. s ∈ y
⊢ s ⊆ s

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  eq  :  EqDecider(T)@i
3.  x  :  Point(face-lattice(T;eq))@i
4.  y  :  Point(face-lattice(T;eq))@i
5.  Point(face-lattice(T;eq))  \msubseteq{}r  fset(fset(T  +  T))
6.  x  \msubseteq{}  y@i
7.  s  :  fset(T  +  T)@i
8.  s  \mmember{}  x@i
\mvdash{}  \mdownarrow{}\mexists{}t:fset(T  +  T).  (t  \mmember{}  y  \mwedge{}  t  \msubseteq{}  s)


By

---

Latex:
((D  0  THEN  D  0  With  \mkleeneopen{}s\mkleeneclose{}  )  THEN  Auto)

---

Home Index