---

Step * of Lemma neg-dM_inc

∀[I:fset(ℕ)]. ∀[x:names(I)].  (¬(<x>) = <1-x> ∈ Point(dM(I)))
BY
{ (Auto THEN RepUR ``dM_inc dM_opp`` 0 THEN (Unfold `dM` 0 THEN RWO "free-dma-point" 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:names(I)].    (\mneg{}(<x>)  =  ə-x>)


By

---

Latex:
(Auto  THEN  RepUR  ``dM\_inc  dM\_opp``  0  THEN  (Unfold  `dM`  0  THEN  RWO  "free-dma-point"  0)  THEN  Auto)

---

Home Index