---

Step * of Lemma finite-powerset-lattice_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[whole:fset(T)].
  finite-powerset-lattice(T;eq;whole) ∈ BoundedDistributiveLattice supposing ∀x:T. x ∈ whole
BY
{ (ProveWfLemma THEN RepUR ``so_apply`` 0 THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. whole : fset(T)
4. ∀x:T. x ∈ whole
5. ∀[a,b:fset(T)].  (λa,b. a ⋂ b[a;b] = λa,b. a ⋂ b[b;a] ∈ fset(T))
6. ∀[a,b:fset(T)].  (λa,b. a ⋃ b[a;b] = λa,b. a ⋃ b[b;a] ∈ fset(T))
7. ∀[a,b,c:fset(T)].  (λa,b. a ⋂ b[a;λa,b. a ⋂ b[b;c]] = λa,b. a ⋂ b[λa,b. a ⋂ b[a;b];c] ∈ fset(T))
8. ∀[a,b,c:fset(T)].  (λa,b. a ⋃ b[a;λa,b. a ⋃ b[b;c]] = λa,b. a ⋃ b[λa,b. a ⋃ b[a;b];c] ∈ fset(T))
9. ∀[a,b:fset(T)].  (λa,b. a ⋃ b[a;λa,b. a ⋂ b[a;b]] = a ∈ fset(T))
10. ∀[a,b:fset(T)].  (λa,b. a ⋂ b[a;λa,b. a ⋃ b[a;b]] = a ∈ fset(T))
11. a : fset(T)
⊢ a ⋂ whole = a ∈ fset(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[whole:fset(T)].
    finite-powerset-lattice(T;eq;whole)  \mmember{}  BoundedDistributiveLattice  supposing  \mforall{}x:T.  x  \mmember{}  whole


By

---

Latex:
(ProveWfLemma  THEN  RepUR  ``so\_apply``  0  THEN  Auto)

---

Home Index