Step
*
of Lemma
nat_add_mon_wf2
<ℕ,+> ∈ OCMon
BY
{ BLemma `inj_into_ocmon` THEN Auto⋅ }
1
∃h:OCMon
 ∃f:|<ℕ,+>| ⟶ |h|
  (IsMonHomInj(<ℕ,+>h;f)
  ∧ RelsIso(|<ℕ,+>|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
  ∧ RelsIso(|<ℕ,+>|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f))
Latex:
Latex:
<\mBbbN{},+>  \mmember{}  OCMon
By
Latex:
BLemma  `inj\_into\_ocmon`  THEN  Auto\mcdot{}
Home
Index