Step
*
2
of Lemma
mk-DeMorgan-algebra_wf
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
BY
{ Assert ⌜L["neg" := n] ∈ DeMorganAlgebraStructure⌝⋅ }
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)))
5. L["neg" := n] ∈ BoundedLatticeStructure
⊢ L["neg" := n] ∈ DeMorganAlgebraStructure
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
6. L["neg" := n] ∈ DeMorganAlgebraStructure
⊢ mk-DeMorgan-algebra(L;n) ∈ DeMorganAlgebra
Latex:
Latex:
1. L : BoundedDistributiveLattice
2. n : Point(L) {}\mrightarrow{} Point(L)
3. \mforall{}x:Point(L). ((n (n x)) = x)
4. (\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))
5. L["neg" := n] \mmember{} BoundedLatticeStructure
\mvdash{} mk-DeMorgan-algebra(L;n) \mmember{} DeMorganAlgebra
By
Latex:
Assert \mkleeneopen{}L["neg" := n] \mmember{} DeMorganAlgebraStructure\mkleeneclose{}\mcdot{}
Home
Index