Step
*
of Lemma
lattice-fset-meet-is-1
No Annotations
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s:fset(Point(l))].
  uiff(/\(s) = 1 ∈ Point(l);∀x:Point(l). (x ∈ s 
⇒ (x = 1 ∈ Point(l))))
BY
{ (InstLemma  `lattice-fset-meet-is-glb` [] THEN RepeatFor 2 (ParallelLast') THEN Auto) }
1
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. ∀[s:fset(Point(l))]. ∀[x:Point(l)].  /\(s) ≤ x supposing x ∈ s
4. ∀[s:fset(Point(l))]. ∀[v:Point(l)].  ((∀x:Point(l). (x ∈ s 
⇒ v ≤ x)) 
⇒ v ≤ /\(s))
5. s : fset(Point(l))
6. /\(s) = 1 ∈ Point(l)
7. x : Point(l)@i
8. x ∈ s
⊢ x = 1 ∈ Point(l)
2
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. ∀[s:fset(Point(l))]. ∀[x:Point(l)].  /\(s) ≤ x supposing x ∈ s
4. ∀[s:fset(Point(l))]. ∀[v:Point(l)].  ((∀x:Point(l). (x ∈ s 
⇒ v ≤ x)) 
⇒ v ≤ /\(s))
5. s : fset(Point(l))
6. ∀x:Point(l). (x ∈ s 
⇒ (x = 1 ∈ Point(l)))
⊢ /\(s) = 1 ∈ Point(l)
Latex:
Latex:
No  Annotations
\mforall{}[l:BoundedLattice].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[s:fset(Point(l))].
    uiff(/\mbackslash{}(s)  =  1;\mforall{}x:Point(l).  (x  \mmember{}  s  {}\mRightarrow{}  (x  =  1)))
By
Latex:
(InstLemma    `lattice-fset-meet-is-glb`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  Auto)
Home
Index