---

Step * 1 of Lemma lattice-extend-order-preserving


1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f : T ⟶ Point(L)
6. x : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
7. y : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
8. fset-ac-le(eq;x;y)
9. ∀a,b:Point(L).  Dec(a = b ∈ Point(L))
10. ∀a,b:Point(L).  Dec(a ≤ b)
⊢ lattice-extend(L;eq;eqL;f;x) ≤ lattice-extend(L;eq;eqL;f;y)
BY
{ (Unfold `lattice-extend` 0
   THEN (InstLemma `lattice-fset-join-is-lub` [⌜L⌝;⌜eqL⌝]⋅ THENA Auto)
   THEN D -1
   THEN BHyp -1 
   THEN Auto
   THEN (RWO "member-fset-image-iff" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN D -1
   THEN (Unhide THENA Auto)
   THEN ExRepD) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f : T ⟶ Point(L)
6. x : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
7. y : {ac:fset(fset(T))| ↑fset-antichain(eq;ac)} 
8. fset-ac-le(eq;x;y)
9. ∀a,b:Point(L).  Dec(a = b ∈ Point(L))
10. ∀a,b:Point(L).  Dec(a ≤ b)
11. ∀[s:fset(Point(L))]. ∀[x:Point(L)].  x ≤ \/(s) supposing x ∈ s
12. ∀[s:fset(Point(L))]. ∀[u:Point(L)].  ((∀x:Point(L). (x ∈ s ⇒ x ≤ u)) ⇒ \/(s) ≤ u)
13. x1 : Point(L)
14. x2 : fset(T)
15. x2 ∈ x
16. x1 = /\(f"(x2)) ∈ Point(L)
⊢ x1 ≤ \/(λxs./\(f"(xs))"(y))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  BoundedDistributiveLattice
4.  eqL  :  EqDecider(Point(L))
5.  f  :  T  {}\mrightarrow{}  Point(L)
6.  x  :  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\} 
7.  y  :  \{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\} 
8.  fset-ac-le(eq;x;y)
9.  \mforall{}a,b:Point(L).    Dec(a  =  b)
10.  \mforall{}a,b:Point(L).    Dec(a  \mleq{}  b)
\mvdash{}  lattice-extend(L;eq;eqL;f;x)  \mleq{}  lattice-extend(L;eq;eqL;f;y)


By

---

Latex:
(Unfold  `lattice-extend`  0
  THEN  (InstLemma  `lattice-fset-join-is-lub`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}eqL\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  BHyp  -1 
  THEN  Auto
  THEN  (RWO  "member-fset-image-iff"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  D  -1
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD)

---

Home Index