Step
*
of Lemma
lattice-fset-join-le
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s:fset(Point(l))]. ∀[x:Point(l)].
(\/(s) ≤ x
⇐⇒ ∀p:Point(l). (p ∈ s
⇒ p ≤ x))
BY
{ (InstLemma `lattice-fset-join-is-lub` []
THEN RepeatFor 2 (ParallelLast')
THEN D -1
THEN Auto
THEN InstLemma `lattice-le_transitivity` [⌜l⌝;⌜p⌝;⌜\/(s)⌝;⌜x⌝]⋅
THEN Auto) }
Latex:
Latex:
\mforall{}[l:BoundedLattice]. \mforall{}[eq:EqDecider(Point(l))]. \mforall{}[s:fset(Point(l))]. \mforall{}[x:Point(l)].
(\mbackslash{}/(s) \mleq{} x \mLeftarrow{}{}\mRightarrow{} \mforall{}p:Point(l). (p \mmember{} s {}\mRightarrow{} p \mleq{} x))
By
Latex:
(InstLemma `lattice-fset-join-is-lub` []
THEN RepeatFor 2 (ParallelLast')
THEN D -1
THEN Auto
THEN InstLemma `lattice-le\_transitivity` [\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}\mbackslash{}/(s)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index