---

Step * of Lemma range_sup-const

∀I:{I:Interval| icompact(I)} . ∀[c:ℝ]. (sup{c | x ∈ I} = c)
BY
{ (InstLemma `range_sup-bound` []
   THEN ParallelLast'
   THEN (D 0 THENA Auto)
   THEN (InstHyp [⌜λ2x.c⌝;⌜c⌝] (-2)⋅ THENA Auto)
   THEN (InstLemma `range_sup-property` [⌜I⌝;λ2x.c]⋅ THENA Auto)
   THEN D -1
   THEN (Assert ⌜c ≤ sup{c | x ∈ I}⌝⋅ THENM EAuto 1)) }

1
.....assertion..... 
1. I : {I:Interval| icompact(I)} 
2. ∀f:{f:I ⟶ℝ| ifun(f;I)} . ∀[c:ℝ]. sup{f[x] | x ∈ I} ≤ c supposing ∀x:ℝ. ((x ∈ I) ⇒ (f[x] ≤ c))
3. c : ℝ
4. sup{c | x ∈ I} ≤ c
5. c(x∈I) ≤ sup{c | x ∈ I}
6. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ c(x∈I)) ∧ ((sup{c | x ∈ I} - e) < x))))
⊢ c ≤ sup{c | x ∈ I}

---

Latex:

---

Latex:
\mforall{}I:\{I:Interval|  icompact(I)\}  .  \mforall{}[c:\mBbbR{}].  (sup\{c  |  x  \mmember{}  I\}  =  c)


By

---

Latex:
(InstLemma  `range\_sup-bound`  []
  THEN  ParallelLast'
  THEN  (D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}x.c\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `range\_sup-property`  [\mkleeneopen{}I\mkleeneclose{};\mlambda{}\msubtwo{}x.c]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (Assert  \mkleeneopen{}c  \mleq{}  sup\{c  |  x  \mmember{}  I\}\mkleeneclose{}\mcdot{}  THENM  EAuto  1))

---

Home Index