---

Step * of Lemma Inorm-non-neg

∀[I:{I:Interval| icompact(I)} ]. ∀[f:I ⟶ℝ]. ∀[mc:f[x] continuous for x ∈ I].  (r0 ≤ ||f[x]||_I)
BY
{ (Auto THEN Unfold `Inorm` 0 THEN (InstLemma `range-sup-property` [⌜I⌝;⌜λ2x.|f[x]|⌝;⌜mc⌝]⋅ THENA Auto) THEN D -1) }

1
1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f[x] continuous for x ∈ I
4. |f[x]|(x∈I) ≤ sup{|f[x]||x ∈ I}
5. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ |f[x]|(x∈I)) ∧ ((sup{|f[x]||x ∈ I} - e) < x))))
⊢ r0 ≤ sup{|f[x]||x ∈ I}

---

Latex:

---

Latex:
\mforall{}[I:\{I:Interval|  icompact(I)\}  ].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].  \mforall{}[mc:f[x]  continuous  for  x  \mmember{}  I].    (r0  \mleq{}  ||f[x]||\_I)


By

---

Latex:
(Auto
  THEN  Unfold  `Inorm`  0
  THEN  (InstLemma  `range-sup-property`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.|f[x]|\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index