---

Step * 2 of Lemma range_sup_functionality2


1. I : {I:Interval| icompact(I)} 
2. J : {I:Interval| icompact(I)} 
3. f : {x:ℝ| x ∈ I}  ⟶ ℝ
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
5. g : {x:ℝ| x ∈ J}  ⟶ ℝ
6. ∀x,y:{x:ℝ| x ∈ J} .  ((x = y) ⇒ (g[x] = g[y]))
7. ∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ J} . (f[x] = g[y])
8. ∀x:{x:ℝ| x ∈ J} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x])
9. x : ℝ
10. x ∈ J
⊢ g[x] ≤ sup{f[x] | x ∈ I}
BY
{ ((D -3 With ⌜x⌝  THENA Auto)
   THEN D -1
   THEN (InstLemma  `rleq-range_sup` [⌜I⌝;⌜f⌝;⌜y⌝]⋅ THENM RWO "-1<" 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  \{I:Interval|  icompact(I)\} 
2.  J  :  \{I:Interval|  icompact(I)\} 
3.  f  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
5.  g  :  \{x:\mBbbR{}|  x  \mmember{}  J\}    {}\mrightarrow{}  \mBbbR{}
6.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  J\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y]))
7.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  (f[x]  =  g[y])
8.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[y]  =  g[x])
9.  x  :  \mBbbR{}
10.  x  \mmember{}  J
\mvdash{}  g[x]  \mleq{}  sup\{f[x]  |  x  \mmember{}  I\}


By

---

Latex:
((D  -3  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  (InstLemma    `rleq-range\_sup`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENM  RWO  "-1<"  0)
  THEN  Auto)

---

Home Index