---

Step * of Lemma range_sup_functionality2

No Annotations
∀I,J:{I:Interval| icompact(I)} . ∀f:{x:ℝ| x ∈ I}  ⟶ ℝ.
  ∀g:{x:ℝ| x ∈ J}  ⟶ ℝ
    (sup{f[x] | x ∈ I} = sup{g[x] | x ∈ J}) supposing 
       (((∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ J} . (f[x] = g[y])) ∧ (∀x:{x:ℝ| x ∈ J} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x]))) and 
       (∀x,y:{x:ℝ| x ∈ J} .  ((x = y) ⇒ (g[x] = g[y])))) 
  supposing ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
BY
{ (Auto THEN BLemma `rleq_antisymmetry` THEN Auto THEN BLemma `range_sup-bound` THEN Auto) }

1
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 ∈ I
⊢ f[x] ≤ sup{g[x] | x ∈ J}

2
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}

---

Latex:

---

Latex:
No  Annotations
\mforall{}I,J:\{I:Interval|  icompact(I)\}  .  \mforall{}f:\{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}.
    \mforall{}g:\{x:\mBbbR{}|  x  \mmember{}  J\}    {}\mrightarrow{}  \mBbbR{}
        (sup\{f[x]  |  x  \mmember{}  I\}  =  sup\{g[x]  |  x  \mmember{}  J\})  supposing 
              (((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  (f[x]  =  g[y]))
              \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[y]  =  g[x])))  and 
              (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  J\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y])))) 
    supposing  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))


By

---

Latex:
(Auto  THEN  BLemma  `rleq\_antisymmetry`  THEN  Auto  THEN  BLemma  `range\_sup-bound`  THEN  Auto)

---

Home Index