Step
*
of Lemma
lattice-fset-join-is-lub
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))].
((∀[s:fset(Point(l))]. ∀[x:Point(l)]. x ≤ \/(s) supposing x ∈ s)
∧ (∀[s:fset(Point(l))]. ∀[u:Point(l)]. ((∀x:Point(l). (x ∈ s
⇒ x ≤ u))
⇒ \/(s) ≤ u)))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN MoveToConcl (-1)) }
1
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
⊢ ∀s:fset(Point(l)). ∀[x:Point(l)]. x ≤ \/(s) supposing x ∈ s
2
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
⊢ ∀s:fset(Point(l)). ∀[u:Point(l)]. ((∀x:Point(l). (x ∈ s
⇒ x ≤ u))
⇒ \/(s) ≤ u)
Latex:
Latex:
\mforall{}[l:BoundedLattice]. \mforall{}[eq:EqDecider(Point(l))].
((\mforall{}[s:fset(Point(l))]. \mforall{}[x:Point(l)]. x \mleq{} \mbackslash{}/(s) supposing x \mmember{} s)
\mwedge{} (\mforall{}[s:fset(Point(l))]. \mforall{}[u:Point(l)]. ((\mforall{}x:Point(l). (x \mmember{} s {}\mRightarrow{} x \mleq{} u)) {}\mRightarrow{} \mbackslash{}/(s) \mleq{} u)))
By
Latex:
(RepeatFor 4 ((D 0 THENA Auto)) THEN MoveToConcl (-1))
Home
Index