Step
*
1
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;b);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;b);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;b);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