---

Step * 1 of Lemma ni-max-nat


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

1
1. n : ℕ
2. m : ℕ
3. x : ℕ
⊢ ↑(x <z n ∨bx <z m) ⇐⇒ ↑x <z imax(n;m)

---

Latex:

---

Latex:

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


By

---

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

---

Home Index