Step
*
2
2
1
1
2
1
1
of Lemma
fl-meet-0-1
1. v : BoundedDistributiveLattice
2. ee : EqDecider(Point(v))
3. a : Point(v)
4. b : Point(v)
5. /\({}) ∧ a ∧ b = 0 ∈ Point(v)
⊢ a ∧ b = 0 ∈ Point(v)
BY
{ (RepUR ``lattice-fset-meet empty-fset`` -1 THEN NthHypEq (-1) THEN EqCD THEN Auto) }
Latex:
Latex:
1. v : BoundedDistributiveLattice
2. ee : EqDecider(Point(v))
3. a : Point(v)
4. b : Point(v)
5. /\mbackslash{}(\{\}) \mwedge{} a \mwedge{} b = 0
\mvdash{} a \mwedge{} b = 0
By
Latex:
(RepUR ``lattice-fset-meet empty-fset`` -1 THEN NthHypEq (-1) THEN EqCD THEN Auto)
Home
Index