---

Step * of Lemma mk-DeMorgan-algebra_wf

∀[L:BoundedDistributiveLattice]. ∀[n:Point(L) ⟶ Point(L)].
  mk-DeMorgan-algebra(L;n) ∈ DeMorganAlgebra 
  supposing (∀x:Point(L). ((n (n x)) = x ∈ Point(L)))
  ∧ ((∀x,y:Point(L).  ((n x ∧ y) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) = n x ∧ n y ∈ Point(L))))
BY
{ (Auto THEN Assert ⌜L["neg" := n] ∈ BoundedLatticeStructure⌝⋅) }

1
.....assertion..... 
1. L : BoundedDistributiveLattice
2. n : Point(L) ⟶ Point(L)
3. ∀x:Point(L). ((n (n x)) = x ∈ Point(L))
4. (∀x,y:Point(L).  ((n x ∧ y) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) = n x ∧ n y ∈ Point(L)))
⊢ L["neg" := n] ∈ BoundedLatticeStructure

2
1. L : BoundedDistributiveLattice
2. n : Point(L) ⟶ Point(L)
3. ∀x:Point(L). ((n (n x)) = x ∈ Point(L))
4. (∀x,y:Point(L).  ((n x ∧ y) = n x ∨ n y ∈ Point(L))) ∨ (∀x,y:Point(L).  ((n x ∨ y) = n x ∧ n y ∈ Point(L)))
5. L["neg" := n] ∈ BoundedLatticeStructure
⊢ mk-DeMorgan-algebra(L;n) ∈ DeMorganAlgebra

---

Latex:

---

Latex:
\mforall{}[L:BoundedDistributiveLattice].  \mforall{}[n:Point(L)  {}\mrightarrow{}  Point(L)].
    mk-DeMorgan-algebra(L;n)  \mmember{}  DeMorganAlgebra 
    supposing  (\mforall{}x:Point(L).  ((n  (n  x))  =  x))
    \mwedge{}  ((\mforall{}x,y:Point(L).    ((n  x  \mwedge{}  y)  =  n  x  \mvee{}  n  y))  \mvee{}  (\mforall{}x,y:Point(L).    ((n  x  \mvee{}  y)  =  n  x  \mwedge{}  n  y)))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}L["neg"  :=  n]  \mmember{}  BoundedLatticeStructure\mkleeneclose{}\mcdot{})

---

Home Index