---

Step * 1 1 1 of Lemma rmin-idempotent-eq


1. x : ℝ
2. x1 : ℕ+
3. v : ℤ
4. (x x1) = v ∈ ℤ
⊢ imin(v;v) = v ∈ ℤ
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  x1  :  \mBbbN{}\msupplus{}
3.  v  :  \mBbbZ{}
4.  (x  x1)  =  v
\mvdash{}  imin(v;v)  =  v


By

---

Latex:
EAuto  1

---

Home Index