---

Step * of Lemma range-sup-property

∀I:{I:Interval| icompact(I)} . ∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I.  sup(f[x](x∈I)) = sup{f[x]|x ∈ I}
BY
{ xxx(xxx(All (Unfold `so_apply`) THEN Auto)xxx THEN Unfold `range-sup` 0 THEN GenConclAtAddr [2;1;1;1] )xxx }

1
1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f x continuous for x ∈ I
4. v : ∀f:I ⟶ℝ. (f[x] continuous for x ∈ I ⇒ (∃y:ℝ. sup(f(x)(x∈I)) = y))
5. (TERMOF{sup-range:o, 1:l} I) = v ∈ (∀f:I ⟶ℝ. (f[x] continuous for x ∈ I ⇒ (∃y:ℝ. sup(f(x)(x∈I)) = y)))
⊢ sup(f x(x∈I)) = fst((v (λx.(f x)) mc))

---

Latex:

---

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


By

---

Latex:
xxx(xxx(All  (Unfold  `so\_apply`)  THEN  Auto)xxx
        THEN  Unfold  `range-sup`  0
        THEN  GenConclAtAddr  [2;1;1;1]  )xxx

---

Home Index