---

Step * 1 of Lemma ni-min-nat


1. n : ℕ
2. m : ℕ
⊢ ni-min(n∞;m∞) = imin(n;m)∞ ∈ (ℕ ⟶ 𝔹)
BY
{ (Ext THEN RepUR ``ni-min nat2inf`` 0 THEN Auto THEN (BLemma `iff_imp_equal_bool` THENA Auto)) }

1
1. n : ℕ
2. m : ℕ
3. x : ℕ
⊢ ↑(x <z n ∧b x <z m) ⇐⇒ ↑x <z imin(n;m)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
\mvdash{}  ni-min(n\minfty{};m\minfty{})  =  imin(n;m)\minfty{}


By

---

Latex:
(Ext  THEN  RepUR  ``ni-min  nat2inf``  0  THEN  Auto  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto))

---

Home Index