---

Step * 2 1 2 of Lemma l_all_exists_max


1. [A] : Type
2. [R] : A ⟶ ℤ ⟶ ℙ
3. ∀x:A. ∀n,m:ℤ.  (R[x;n] ⇒ R[x;m] supposing n ≤ m)@i
4. u : A@i
5. v : A List@i
6. n1 : ℤ@i
7. R[u;n1]@i
8. (∀x∈v.∃n:ℤ. R[x;n])@i
9. n : ℤ@i
10. (∀x∈v.R[x;n])@i
11. R[u;imax(n1;n)]
⊢ (∀x∈v.R[x;imax(n1;n)])
BY
{ (Thin (-1) THEN RepeatFor 3 (ParallelLast) THEN InstHyp [⌜v[i]⌝;⌜n⌝;⌜imax(n1;n)⌝] 3⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [R]  :  A  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:A.  \mforall{}n,m:\mBbbZ{}.    (R[x;n]  {}\mRightarrow{}  R[x;m]  supposing  n  \mleq{}  m)@i
4.  u  :  A@i
5.  v  :  A  List@i
6.  n1  :  \mBbbZ{}@i
7.  R[u;n1]@i
8.  (\mforall{}x\mmember{}v.\mexists{}n:\mBbbZ{}.  R[x;n])@i
9.  n  :  \mBbbZ{}@i
10.  (\mforall{}x\mmember{}v.R[x;n])@i
11.  R[u;imax(n1;n)]
\mvdash{}  (\mforall{}x\mmember{}v.R[x;imax(n1;n)])


By

---

Latex:
(Thin  (-1)  THEN  RepeatFor  3  (ParallelLast)  THEN  InstHyp  [\mkleeneopen{}v[i]\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}imax(n1;n)\mkleeneclose{}]  3\mcdot{}  THEN  Auto)

---

Home Index