---

Step * 1 1 1 2 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)@i
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)].  /\(s) ≤ x supposing x ∈ s
21. ∀[s:fset(Point(L))]. ∀[v:Point(L)].  ((∀x:Point(L). (x ∈ s ⇒ v ≤ x)) ⇒ v ≤ /\(s))
22. x3 : Point(L)@i
23. x3 ∈ f"(b)
⊢ /\(f"(x2)) ≤ x3
BY
{ (BHyp -4 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)@i
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)].  /\(s) ≤ x supposing x ∈ s
21. ∀[s:fset(Point(L))]. ∀[v:Point(L)].  ((∀x:Point(L). (x ∈ s ⇒ v ≤ x)) ⇒ v ≤ /\(s))
22. x3 : Point(L)@i
23. x3 ∈ f"(b)
⊢ x3 ∈ f"(x2)

---

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)@i
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
20.  \mforall{}[s:fset(Point(L))].  \mforall{}[x:Point(L)].    /\mbackslash{}(s)  \mleq{}  x  supposing  x  \mmember{}  s
21.  \mforall{}[s:fset(Point(L))].  \mforall{}[v:Point(L)].    ((\mforall{}x:Point(L).  (x  \mmember{}  s  {}\mRightarrow{}  v  \mleq{}  x))  {}\mRightarrow{}  v  \mleq{}  /\mbackslash{}(s))
22.  x3  :  Point(L)@i
23.  x3  \mmember{}  f"(b)
\mvdash{}  /\mbackslash{}(f"(x2))  \mleq{}  x3


By

---

Latex:
(BHyp  -4  THEN  Auto)

---

Home Index