Step
*
of Lemma
lattice-fset-meet_wf
No Annotations
∀[l:BoundedLattice]. ((∀x,y:Point(l). Dec(x = y ∈ Point(l)))
⇒ (∀[s:fset(Point(l))]. (/\(s) ∈ Point(l))))
BY
{ (Auto THEN Assert ⌜EqDecider(Point(l))⌝⋅) }
1
.....assertion.....
1. l : BoundedLattice
2. ∀x,y:Point(l). Dec(x = y ∈ Point(l))
3. s : fset(Point(l))
⊢ EqDecider(Point(l))
2
1. l : BoundedLattice
2. ∀x,y:Point(l). Dec(x = y ∈ Point(l))
3. s : fset(Point(l))
4. EqDecider(Point(l))
⊢ /\(s) ∈ Point(l)
Latex:
Latex:
No Annotations
\mforall{}[l:BoundedLattice]. ((\mforall{}x,y:Point(l). Dec(x = y)) {}\mRightarrow{} (\mforall{}[s:fset(Point(l))]. (/\mbackslash{}(s) \mmember{} Point(l))))
By
Latex:
(Auto THEN Assert \mkleeneopen{}EqDecider(Point(l))\mkleeneclose{}\mcdot{})
Home
Index