---

Step * of Lemma shadow-inequalities_wf

No Annotations
∀[n:ℕ]. ∀[ineqs:{L:ℤ List| ||L|| = n ∈ ℤ}  List]. ∀[i:ℕn].
  (shadow-inequalities(i;ineqs) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ}  List)
BY
{ Auto }

1
1. n : ℕ
2. ineqs : {L:ℤ List| ||L|| = n ∈ ℤ}  List
3. i : ℕn
⊢ shadow-inequalities(i;ineqs) ∈ {L:ℤ List| ||L|| = (n - 1) ∈ ℤ}  List

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[ineqs:\{L:\mBbbZ{}  List|  ||L||  =  n\}    List].  \mforall{}[i:\mBbbN{}n].
    (shadow-inequalities(i;ineqs)  \mmember{}  \{L:\mBbbZ{}  List|  ||L||  =  (n  -  1)\}    List)


By

---

Latex:
Auto

---

Home Index