---

Step * of Lemma int_mag_well_founded

WellFnd{i}(ℤ;x,y.|x| < |y|)
BY
{ (InstLemma `inv_image_ind` [⌜parm{i}⌝;⌜ℕ⌝;⌜λ2x y.x < y⌝;⌜ℤ⌝;⌜λx.|x|⌝] THENA Auto) }

1
1. WellFnd{i}(ℤ;x,y.(λx.|x|) x < (λx.|x|) y)
⊢ WellFnd{i}(ℤ;x,y.|x| < |y|)

---

Latex:

---

Latex:
WellFnd\{i\}(\mBbbZ{};x,y.|x|  <  |y|)


By

---

Latex:
(InstLemma  `inv\_image\_ind`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x  <  y\mkleeneclose{};\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}x.|x|\mkleeneclose{}]  THENA  Auto)

---

Home Index