---

Step * 1 of Lemma rmaximum_functionality_wrt_rleq


1. n : ℤ
2. k : ℤ
⊢ ∀x,y:{n..(n + 0) + 1-} ⟶ ℝ.  ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + 0)) ⇒ (x[k@0] ≤ y[k@0]))) ⇒ (x[n] ≤ y[n]))
BY
{ Auto⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  k  :  \mBbbZ{}
\mvdash{}  \mforall{}x,y:\{n..(n  +  0)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.
        ((\mforall{}k@0:\mBbbZ{}.  ((n  \mleq{}  k@0)  {}\mRightarrow{}  (k@0  \mleq{}  (n  +  0))  {}\mRightarrow{}  (x[k@0]  \mleq{}  y[k@0])))  {}\mRightarrow{}  (x[n]  \mleq{}  y[n]))


By

---

Latex:
Auto\mcdot{}

---

Home Index