---

Step * of Lemma fset-ac-glb-is-glb

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
  greatest-lower-bound({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2);ac1;ac2;fset-ac-glb(eq\000C;ac1;ac2))
BY
{ (Auto THEN D 0 THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. ac1 : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
4. ac2 : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
⊢ fset-ac-le(eq;fset-ac-glb(eq;ac1;ac2);ac1)

2
1. T : Type
2. eq : EqDecider(T)
3. ac1 : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
4. ac2 : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
⊢ fset-ac-le(eq;fset-ac-glb(eq;ac1;ac2);ac2)

3
1. T : Type
2. eq : EqDecider(T)
3. ac1 : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
4. ac2 : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
5. fset-ac-le(eq;fset-ac-glb(eq;ac1;ac2);ac2)
6. ac1@0 : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
7. fset-ac-le(eq;ac1@0;ac1)
8. fset-ac-le(eq;ac1@0;ac2)
⊢ fset-ac-le(eq;ac1@0;fset-ac-glb(eq;ac1;ac2))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[ac1,ac2:\{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  ].
    greatest-lower-bound(\{ac:fset(fset(T))| 
                                                \muparrow{}fset-antichain(eq;ac)\}  ;ac1,ac2.fset-ac-le(eq;ac1;ac2);ac1;ac2;fset-ac-glb(\000Ceq;ac1;ac2))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index