Step
*
of Lemma
rleq-iff4
∀[x,y:ℝ].  (x ≤ y 
⇐⇒ ∀n:ℕ+. ((x n) ≤ ((y n) + 4)))
BY
{ Auto }
1
1. x : ℝ
2. y : ℝ
3. x ≤ y@i
4. n : ℕ+@i
⊢ (x n) ≤ ((y n) + 4)
2
1. x : ℝ
2. y : ℝ
3. ∀n:ℕ+. ((x n) ≤ ((y n) + 4))@i
⊢ x ≤ y
Latex:
Latex:
\mforall{}[x,y:\mBbbR{}].    (x  \mleq{}  y  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  \mleq{}  ((y  n)  +  4)))
By
Latex:
Auto
Home
Index