Step * 2 of Lemma mu-ge_wf2


1. : ℤ
2. {n...} ⟶ (Top Top)
3. {n...}
4. ↑isl(f m)
5. ∀d:ℕ((n ≤ (m d))  (mu-ge(f;m d) ∈ {n...}))
⊢ mu-ge(f;n) ∈ {n...}
BY
((InstHyp [⌜n⌝(-1)⋅ THENA Auto) THEN NthHypSq (-1) THEN RepeatFor (EqCD) THEN Auto) }


Latex:


Latex:

1.  n  :  \mBbbZ{}
2.  f  :  \{n...\}  {}\mrightarrow{}  (Top  +  Top)
3.  m  :  \{n...\}
4.  \muparrow{}isl(f  m)
5.  \mforall{}d:\mBbbN{}.  ((n  \mleq{}  (m  -  d))  {}\mRightarrow{}  (mu-ge(f;m  -  d)  \mmember{}  \{n...\}))
\mvdash{}  mu-ge(f;n)  \mmember{}  \{n...\}


By


Latex:
((InstHyp  [\mkleeneopen{}m  -  n\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  NthHypSq  (-1)  THEN  RepeatFor  2  (EqCD)  THEN  Auto)




Home Index