---

Step * of Lemma sq_stable__ex_int_seg_ap

∀n,m:ℤ. ∀f:{n..m-} ⟶ 𝔹.  SqStable(∃k:{n..m-}. (↑(f k)))
BY
{ ((Auto THEN D 0 THEN Auto)
   THEN UseWitness ⌜<mu-ge(f;n), Ax>⌝⋅
   THEN D -1
   THEN (FLemma `mu-ge-bound` [-1] THENA Auto)
   THEN FLemma `mu-ge-bound-property` [-2]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.  \mforall{}f:\{n..m\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}.    SqStable(\mexists{}k:\{n..m\msupminus{}\}.  (\muparrow{}(f  k)))


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)
  THEN  UseWitness  \mkleeneopen{}<mu-ge(f;n),  Ax>\mkleeneclose{}\mcdot{}
  THEN  D  -1
  THEN  (FLemma  `mu-ge-bound`  [-1]  THENA  Auto)
  THEN  FLemma  `mu-ge-bound-property`  [-2]
  THEN  Auto)

---

Home Index