---

Step * 1 6 of Lemma nat_add_mon_wf2

.....wf..... 
1. f : |<ℕ,+>| ⟶ |<ℤ+>|
⊢ IsMonHomInj(<ℕ,+>;<ℤ+>;f)
  ∧ RelsIso(|<ℕ,+>|;|<ℤ+>|;x,y.↑(x =b y);x,y.↑(x =b y);f)
  ∧ RelsIso(|<ℕ,+>|;|<ℤ+>|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f) ∈ ℙ
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  f  :  |<\mBbbN{},+>|  {}\mrightarrow{}  |<\mBbbZ{}+>|
\mvdash{}  IsMonHomInj(<\mBbbN{},+><\mBbbZ{}+>f)
    \mwedge{}  RelsIso(|<\mBbbN{},+>|;|<\mBbbZ{}+>|;x,y.\muparrow{}(x  =\msubb{}  y);x,y.\muparrow{}(x  =\msubb{}  y);f)
    \mwedge{}  RelsIso(|<\mBbbN{},+>|;|<\mBbbZ{}+>|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);f)  \mmember{}  \mBbbP{}


By

---

Latex:
Auto

---

Home Index