---

Step * 1 1 1 of Lemma lattice-extend-meet


1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f : T ⟶ Point(L)
6. as : fset(fset(T))@i
7. bs : fset(fset(T))@i
8. ∀a,b:Point(L).  Dec(a = b ∈ Point(L))
9. ∀a,b:Point(L).  Dec(a ≤ b)
⊢ fset-ac-le(eq;as;bs) ⇒ \/(λxs./\(f"(xs))"(as)) ≤ \/(λxs./\(f"(xs))"(bs))
BY
{ ((D 0 THENA Auto) THEN (FLemma  `fset-ac-le-implies2` [-1]⋅ THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f : T ⟶ Point(L)
6. as : fset(fset(T))@i
7. bs : fset(fset(T))@i
8. ∀a,b:Point(L).  Dec(a = b ∈ Point(L))
9. ∀a,b:Point(L).  Dec(a ≤ b)
10. fset-ac-le(eq;as;bs)
11. ∀a:fset(T). (a ∈ as ⇒ (↓∃b:fset(T). (b ∈ bs ∧ b ⊆ a)))
⊢ \/(λxs./\(f"(xs))"(as)) ≤ \/(λxs./\(f"(xs))"(bs))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  BoundedDistributiveLattice
4.  eqL  :  EqDecider(Point(L))
5.  f  :  T  {}\mrightarrow{}  Point(L)
6.  as  :  fset(fset(T))@i
7.  bs  :  fset(fset(T))@i
8.  \mforall{}a,b:Point(L).    Dec(a  =  b)
9.  \mforall{}a,b:Point(L).    Dec(a  \mleq{}  b)
\mvdash{}  fset-ac-le(eq;as;bs)  {}\mRightarrow{}  \mbackslash{}/(\mlambda{}xs./\mbackslash{}(f"(xs))"(as))  \mleq{}  \mbackslash{}/(\mlambda{}xs./\mbackslash{}(f"(xs))"(bs))


By

---

Latex:
((D  0  THENA  Auto)  THEN  (FLemma    `fset-ac-le-implies2`  [-1]\mcdot{}  THENA  Auto))

---

Home Index