---

Step * 1 of Lemma lattice-extend-1


1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f : T ⟶ Point(L)
⊢ lattice-extend(L;eq;eqL;f;1) = 1 ∈ Point(L)
BY
{ (RepUR ``lattice-1 free-dist-lattice mk-bounded-distributive-lattice mk-bounded-lattice lattice-extend`` 0
   THEN (RWO "fset-image-singleton" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst' f"({}) ~ {} 0 THENA (RepUR ``fset-image empty-fset f-union`` 0 THEN Auto))
   THEN (RepUR ``lattice-fset-meet empty-fset`` 0 THEN RepUR ``lattice-fset-join fset-singleton`` 0)
   THEN Fold `lattice-1` 0) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. f : T ⟶ Point(L)
⊢ 1 ∨ 0 = 1 ∈ Point(L)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  BoundedDistributiveLattice
4.  eqL  :  EqDecider(Point(L))
5.  f  :  T  {}\mrightarrow{}  Point(L)
\mvdash{}  lattice-extend(L;eq;eqL;f;1)  =  1


By

---

Latex:
(...
  THEN  (RWO  "fset-image-singleton"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst'  f"(\{\})  \msim{}  \{\}  0  THENA  (RepUR  ``fset-image  empty-fset  f-union``  0  THEN  Auto))
  THEN  (RepUR  ``lattice-fset-meet  empty-fset``  0  THEN  RepUR  ``lattice-fset-join  fset-singleton``  0)
  THEN  Fold  `lattice-1`  0)

---

Home Index