---

Step * of Lemma infn-nonneg

∀[I:{I:Interval| icompact(I)} ]
  ∀n:ℕ. ∀f:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} .
    r0 ≤ (infn(n;I) f) supposing ∀a:I^n. (r0 ≤ (f a))
BY
{ (Auto THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[I:\{I:Interval|  icompact(I)\}  ]
    \mforall{}n:\mBbbN{}.  \mforall{}f:\{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}|  \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\}  .
        r0  \mleq{}  (infn(n;I)  f)  supposing  \mforall{}a:I\^{}n.  (r0  \mleq{}  (f  a))


By

---

Latex:
(Auto  THEN  EAuto  1)

---

Home Index