---

Step * 1 of Lemma dMpair-eq-meet


1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. i ∈ I
5. j ∈ I
⊢ dMpair(i;j) = <i> ∧ <j> ∈ Point(dM(I))
BY
{ (RepUR ``dMpair lattice-meet dM_inc dM free-DeMorgan-algebra`` 0
   THEN RepUR ``mk-DeMorgan-algebra free-DeMorgan-lattice free-dist-lattice`` 0
   THEN RepUR ``mk-bounded-distributive-lattice mk-bounded-lattice`` 0
   THEN ((RepUR ``lattice-point`` 0 THEN EqTypeCD) THENA Auto)
   THEN Try ((Using [`T', ⌜names(I) + names(I)⌝] (BLemma `fset-antichain-singleton`)⋅ THEN Auto))) }

1
1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. i ∈ I
5. j ∈ I
⊢ {{inl i,inl j}}
= fset-ac-glb(union-deq(names(I);names(I);NamesDeq;NamesDeq);<i>;<j>)
∈ fset(fset(names(I) + names(I)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
3.  j  :  \mBbbN{}
4.  i  \mmember{}  I
5.  j  \mmember{}  I
\mvdash{}  dMpair(i;j)  =  <i>  \mwedge{}  <j>


By

---

Latex:
(RepUR  ``dMpair  lattice-meet  dM\_inc  dM  free-DeMorgan-algebra``  0
  THEN  RepUR  ``mk-DeMorgan-algebra  free-DeMorgan-lattice  free-dist-lattice``  0
  THEN  RepUR  ``mk-bounded-distributive-lattice  mk-bounded-lattice``  0
  THEN  ((RepUR  ``lattice-point``  0  THEN  EqTypeCD)  THENA  Auto)
  THEN  Try  ((Using  [`T',  \mkleeneopen{}names(I)  +  names(I)\mkleeneclose{}]  (BLemma  `fset-antichain-singleton`)\mcdot{}  THEN  Auto)))

---

Home Index