---

Step * of Lemma range_sup_functionality

No Annotations
∀I:{I:Interval| icompact(I)} . ∀f:{x:ℝ| x ∈ I}  ⟶ ℝ.
  ∀g:{x:ℝ| x ∈ I}  ⟶ ℝ. sup{f[x] | x ∈ I} = sup{g[x] | x ∈ I} supposing ∀x:{x:ℝ| x ∈ I} . (f[x] = g[x]) 
  supposing ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
BY
{ (InstLemma `range_sup_functionality2` []
   THEN ParallelLast'
   THEN (D -1 With ⌜I⌝  THENA Auto)
   THEN ParallelLast'
   THEN Intro
   THEN (D -2 THENA Auto)
   THEN ParallelLast
   THEN Intro
   THEN BackThruSomeHyp) }

1
1. I : {I:Interval| icompact(I)} 
2. f : {x:ℝ| x ∈ I}  ⟶ ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
4. ∀g:{x:ℝ| x ∈ I}  ⟶ ℝ
     (sup{f[x] | x ∈ I} = sup{g[x] | x ∈ I}) supposing 
        (((∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[x] = g[y])) ∧ (∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x]))) and\000C 
        (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))))
5. g : {x:ℝ| x ∈ I}  ⟶ ℝ
6. (sup{f[x] | x ∈ I} = sup{g[x] | x ∈ I}) supposing 
      (((∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[x] = g[y])) ∧ (∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x]))) and 
      (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))))
7. ∀x:{x:ℝ| x ∈ I} . (f[x] = g[x])
⊢ ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))

2
1. I : {I:Interval| icompact(I)} 
2. f : {x:ℝ| x ∈ I}  ⟶ ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
4. ∀g:{x:ℝ| x ∈ I}  ⟶ ℝ
     (sup{f[x] | x ∈ I} = sup{g[x] | x ∈ I}) supposing 
        (((∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[x] = g[y])) ∧ (∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x]))) and\000C 
        (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))))
5. g : {x:ℝ| x ∈ I}  ⟶ ℝ
6. (sup{f[x] | x ∈ I} = sup{g[x] | x ∈ I}) supposing 
      (((∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[x] = g[y])) ∧ (∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x]))) and 
      (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))))
7. ∀x:{x:ℝ| x ∈ I} . (f[x] = g[x])
⊢ (∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[x] = g[y])) ∧ (∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x]))

---

Latex:

---

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


By

---

Latex:
(InstLemma  `range\_sup\_functionality2`  []
  THEN  ParallelLast'
  THEN  (D  -1  With  \mkleeneopen{}I\mkleeneclose{}    THENA  Auto)
  THEN  ParallelLast'
  THEN  Intro
  THEN  (D  -2  THENA  Auto)
  THEN  ParallelLast
  THEN  Intro
  THEN  BackThruSomeHyp)

---

Home Index