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 ∈  (x 1 ∈ Point(l))))
BY
(InstLemma  `lattice-fset-meet-is-glb` [] THEN RepeatFor (ParallelLast') THEN Auto) }

1
1. BoundedLattice
2. eq EqDecider(Point(l))
3. ∀[s:fset(Point(l))]. ∀[x:Point(l)].  /\(s) ≤ supposing x ∈ s
4. ∀[s:fset(Point(l))]. ∀[v:Point(l)].  ((∀x:Point(l). (x ∈  v ≤ x))  v ≤ /\(s))
5. fset(Point(l))
6. /\(s) 1 ∈ Point(l)
7. Point(l)@i
8. x ∈ s
⊢ 1 ∈ Point(l)

2
1. BoundedLattice
2. eq EqDecider(Point(l))
3. ∀[s:fset(Point(l))]. ∀[x:Point(l)].  /\(s) ≤ supposing x ∈ s
4. ∀[s:fset(Point(l))]. ∀[v:Point(l)].  ((∀x:Point(l). (x ∈  v ≤ x))  v ≤ /\(s))
5. fset(Point(l))
6. ∀x:Point(l). (x ∈  (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