---

Step * 1 1 1 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)
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)
17. b : fset(T)
18. b ∈ y
19. b ⊆ x2
⊢ /\(f"(b)) ≤ \/(λxs./\(f"(xs))"(y))
BY
{ ((InstLemma `lattice-fset-join-is-lub` [⌜L⌝;⌜eqL⌝]⋅ THENA Auto) THEN D -1 THEN BHyp -2  THEN Auto) }

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)
17. b : fset(T)
18. b ∈ y
19. b ⊆ x2
20. ∀[s:fset(Point(L))]. ∀[x:Point(L)].  x ≤ \/(s) supposing x ∈ s
21. ∀[s:fset(Point(L))]. ∀[u:Point(L)].  ((∀x:Point(L). (x ∈ s ⇒ x ≤ u)) ⇒ \/(s) ≤ u)
⊢ /\(f"(b)) ∈ λ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)
11.  \mforall{}[s:fset(Point(L))].  \mforall{}[x:Point(L)].    x  \mleq{}  \mbackslash{}/(s)  supposing  x  \mmember{}  s
12.  \mforall{}[s:fset(Point(L))].  \mforall{}[u:Point(L)].    ((\mforall{}x:Point(L).  (x  \mmember{}  s  {}\mRightarrow{}  x  \mleq{}  u))  {}\mRightarrow{}  \mbackslash{}/(s)  \mleq{}  u)
13.  x1  :  Point(L)
14.  x2  :  fset(T)
15.  x2  \mmember{}  x
16.  x1  =  /\mbackslash{}(f"(x2))
17.  b  :  fset(T)
18.  b  \mmember{}  y
19.  b  \msubseteq{}  x2
\mvdash{}  /\mbackslash{}(f"(b))  \mleq{}  \mbackslash{}/(\mlambda{}xs./\mbackslash{}(f"(xs))"(y))


By

---

Latex:
((InstLemma  `lattice-fset-join-is-lub`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}eqL\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  BHyp  -2    THEN  Auto)

---

Home Index