---

Step * of Lemma lattice-meet-join-images-distrib

∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀as,bs:fset(fset(Point(L))).
  (\/(λls./\(ls)"(as)) ∧ \/(λls./\(ls)"(bs))
  = \/(λls./\(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);as;as.λbs.as ⋃ bs"(bs))))
  ∈ Point(L))
BY
{ (Auto
   THEN (InstLemma `lattice-meet-fset-join-distrib` [⌜L⌝;⌜eqL⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THEN Auto)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. L : BoundedDistributiveLattice
2. eqL : EqDecider(Point(L))
3. as : fset(fset(Point(L)))
4. bs : fset(fset(Point(L)))
5. ∀[s1,s2:fset(Point(L))].  (\/(s1) ∧ \/(s2) = \/(f-union(eqL;eqL;s1;a.λb.a ∧ b"(s2))) ∈ Point(L))
⊢ f-union(eqL;eqL;λls./\(ls)"(as);a.λb.a ∧ b"(λls./\(ls)"(bs)))
= λls./\(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);as;as.λbs.as ⋃ bs"(bs)))
∈ fset(Point(L))

---

Latex:

---

Latex:
\mforall{}L:BoundedDistributiveLattice.  \mforall{}eqL:EqDecider(Point(L)).  \mforall{}as,bs:fset(fset(Point(L))).
    (\mbackslash{}/(\mlambda{}ls./\mbackslash{}(ls)"(as))  \mwedge{}  \mbackslash{}/(\mlambda{}ls./\mbackslash{}(ls)"(bs))
    =  \mbackslash{}/(\mlambda{}ls./\mbackslash{}(ls)"(f-union(deq-fset(eqL);deq-fset(eqL);as;as.\mlambda{}bs.as  \mcup{}  bs"(bs)))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `lattice-meet-fset-join-distrib`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}eqL\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THEN  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index