---

Step * 1 of Lemma ni-max-zero


1. x : ℕ∞
2. ni-max(x;0∞) = ni-max(x;0∞) ∈ (ℕ ⟶ 𝔹)
⊢ ni-max(x;0∞) = x ∈ (ℕ ⟶ 𝔹)
BY
{ (Ext⋅ THEN Auto THEN RenameVar `i' (-1) THEN RepUR ``ni-max nat-inf-infinity nat2inf`` 0 THEN AutoBoolCase ⌜x i⌝⋅) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\minfty{}
2.  ni-max(x;0\minfty{})  =  ni-max(x;0\minfty{})
\mvdash{}  ni-max(x;0\minfty{})  =  x


By

---

Latex:
(Ext\mcdot{}
  THEN  Auto
  THEN  RenameVar  `i'  (-1)
  THEN  RepUR  ``ni-max  nat-inf-infinity  nat2inf``  0
  THEN  AutoBoolCase  \mkleeneopen{}x  i\mkleeneclose{}\mcdot{})

---

Home Index