---

Step * of Lemma fset-ac-le-distributive

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b,c:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
  (fset-ac-glb(eq;a;fset-ac-lub(eq;b;c))
  = fset-ac-lub(eq;fset-ac-glb(eq;a;b);fset-ac-glb(eq;a;c))
  ∈ {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} )
BY
{ (Auto
   THEN EqTypeCD
   THEN Auto
   THEN Try (Complete ((GenConclAtAddr [1;2] THEN D -2 THEN Unhide THEN Auto)))
   THEN (InstLemma `least-upper-bound-unique`
         [{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;
         ⌜λ2ac1 ac2.fset-ac-le(eq;ac1;ac2)⌝; ⌜fset-ac-glb(eq;a;b)⌝;⌜fset-ac-glb(eq;a;c)⌝]⋅
         THENA Auto
         )
   THEN BHyp -1
   THEN Auto
   THEN Thin (-1)
   THEN D 0
   THEN Auto) }

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;b);fset-ac-glb(eq;a;fset-ac-lub(eq;b;c)))

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

3
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)} 
6. fset-ac-le(eq;fset-ac-glb(eq;a;c);fset-ac-glb(eq;a;fset-ac-lub(eq;b;c)))
7. x : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
8. fset-ac-le(eq;fset-ac-glb(eq;a;b);x)
9. fset-ac-le(eq;fset-ac-glb(eq;a;c);x)
⊢ fset-ac-le(eq;fset-ac-glb(eq;a;fset-ac-lub(eq;b;c));x)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b,c:\{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  ].
    (fset-ac-glb(eq;a;fset-ac-lub(eq;b;c))  =  fset-ac-lub(eq;fset-ac-glb(eq;a;b);fset-ac-glb(eq;a;c)))


By

---

Latex:
(Auto
  THEN  EqTypeCD
  THEN  Auto
  THEN  Try  (Complete  ((GenConclAtAddr  [1;2]  THEN  D  -2  THEN  Unhide  THEN  Auto)))
  THEN  (InstLemma  `least-upper-bound-unique`
              [\{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  ;
              \mkleeneopen{}\mlambda{}\msubtwo{}ac1  ac2.fset-ac-le(eq;ac1;ac2)\mkleeneclose{};  \mkleeneopen{}fset-ac-glb(eq;a;b)\mkleeneclose{};\mkleeneopen{}fset-ac-glb(eq;a;c)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  BHyp  -1
  THEN  Auto
  THEN  Thin  (-1)
  THEN  D  0
  THEN  Auto)

---

Home Index