---

Step * of Lemma I-norm_wf

No Annotations
∀[I:{I:Interval| icompact(I)} ]. ∀[f:{x:ℝ| x ∈ I}  ⟶ ℝ].
  ||f[x]||_x:I ∈ ℝ supposing ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
BY
{ (Intros
   THEN Unhide
   THEN (Assert ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (|f[x]| = |f[y]|)) BY
               (RepeatFor 3 (ParallelLast) THEN Auto))
   THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:\{I:Interval|  icompact(I)\}  ].  \mforall{}[f:\{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}].
    ||f[x]||\_x:I  \mmember{}  \mBbbR{}  supposing  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (Assert  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (|f[x]|  =  |f[y]|))  BY
                          (RepeatFor  3  (ParallelLast)  THEN  Auto))
  THEN  ProveWfLemma)

---

Home Index