---

Step * 1 of Lemma rmin-idempotent-eq


1. x : ℝ
⊢ x = rmin(x;x) ∈ (ℕ+ ⟶ ℤ)
BY
{ (Symmetry THEN RepUR ``rmin`` 0 THEN (Ext THENA Auto) THEN Reduce 0) }

1
1. x : ℝ
2. x1 : ℕ+
⊢ imin(x x1;x x1) = (x x1) ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
\mvdash{}  x  =  rmin(x;x)


By

---

Latex:
(Symmetry  THEN  RepUR  ``rmin``  0  THEN  (Ext  THENA  Auto)  THEN  Reduce  0)

---

Home Index