---

Step * 2 of Lemma fset-ac-le-distributive


1. T : Type
2. eq : EqDecider(T)
3. a : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
4. b : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
5. c : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
⊢ fset-ac-le(eq;fset-ac-glb(eq;a;c);fset-ac-glb(eq;a;fset-ac-lub(eq;b;c)))
BY
{ ((InstLemma `fset-ac-glb-is-glb` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
   THEN Unfold `greatest-lower-bound` -1
   THEN (BHyp -1 THEN Auto)
   THEN Thin (-1)) }

1
1. T : Type
2. eq : EqDecider(T)
3. a : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
4. b : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
5. c : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
⊢ fset-ac-le(eq;fset-ac-glb(eq;a;c);fset-ac-lub(eq;b;c))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  a  :  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\} 
4.  b  :  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\} 
5.  c  :  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\} 
\mvdash{}  fset-ac-le(eq;fset-ac-glb(eq;a;c);fset-ac-glb(eq;a;fset-ac-lub(eq;b;c)))


By

---

Latex:
((InstLemma  `fset-ac-glb-is-glb`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `greatest-lower-bound`  -1
  THEN  (BHyp  -1  THEN  Auto)
  THEN  Thin  (-1))

---

Home Index