---

Step * 1 1 of Lemma lattice-extend-wc-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))
7. bs : fset(fset(T))
⊢ fset-ac-le(eq;as;bs) ⇒ \/(λxs./\(f"(xs))"(as)) ≤ \/(λxs./\(f"(xs))"(bs))
BY
{ ((Assert ∀a,b:Point(L).  Dec(a = b ∈ Point(L)) BY
          Auto)
   THEN (Assert ∀a,b:Point(L).  Dec(a ≤ b) BY
               (Unfold `lattice-le` 0 THEN 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))
7. bs : fset(fset(T))
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))

---

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))
7.  bs  :  fset(fset(T))
\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:
((Assert  \mforall{}a,b:Point(L).    Dec(a  =  b)  BY
                Auto)
  THEN  (Assert  \mforall{}a,b:Point(L).    Dec(a  \mleq{}  b)  BY
                          (Unfold  `lattice-le`  0  THEN  Auto))
  )

---

Home Index