---

Step * of Lemma interval-fun-maps-compact

No Annotations
∀I,J:Interval. ∀f:I ⟶ℝ.  (interval-fun(I;J;x.f[x]) ⇒ maps-compact(I;J;x.f[x]))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (Assert icompact(i-approx(I;n)) BY
               (Unhide THEN Auto))
   THEN Thin (-2)
   THEN (Assert interval-fun(i-approx(I;n);J;x.f[x]) BY
               (RepeatFor 3 (ParallelOp -3)
                THEN RepeatFor 2 ((ParallelLast THEN Try ((BLemma `i-member-iff` THEN Auto))))
                ))
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜f = g ∈ i-approx(I;n) ⟶ℝ⌝⋅ THENA Auto)
   THEN ThinVar `f'
   THEN MoveToConcl (-1)
   THEN (InstLemma `icompact-is-rccint` [⌜i-approx(I;n)⌝]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN (FLemma `icompact-endpoints-rleq` [-2] THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜left-endpoint(i-approx(I;n)) = a ∈ ℝ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜right-endpoint(i-approx(I;n)) = b ∈ ℝ⌝⋅ THENA Auto)
   THEN ThinVar `I'
   THEN Auto
   THEN (Assert real-fun(g;a;b) BY
               (BLemma `interval-fun-real-fun` THEN Auto))) }

1
1. J : Interval
2. n : ℕ+
3. a : ℝ
4. b : ℝ
5. a ≤ b
6. g : [a, b] ⟶ℝ
7. interval-fun([a, b];J;x.g[x])
8. real-fun(g;a;b)
⊢ ∃m:{m:ℕ+| icompact(i-approx(J;m))} . ∀x:{x:ℝ| x ∈ [a, b]} . (g[x] ∈ i-approx(J;m))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I,J:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.    (interval-fun(I;J;x.f[x])  {}\mRightarrow{}  maps-compact(I;J;x.f[x]))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (Assert  icompact(i-approx(I;n))  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-2)
  THEN  (Assert  interval-fun(i-approx(I;n);J;x.f[x])  BY
                          (RepeatFor  3  (ParallelOp  -3)
                            THEN  RepeatFor  2  ((ParallelLast  THEN  Try  ((BLemma  `i-member-iff`  THEN  Auto))))
                            ))
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}f  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `f'
  THEN  MoveToConcl  (-1)
  THEN  (InstLemma  `icompact-is-rccint`  [\mkleeneopen{}i-approx(I;n)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  (FLemma  `icompact-endpoints-rleq`  [-2]  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}left-endpoint(i-approx(I;n))  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}right-endpoint(i-approx(I;n))  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `I'
  THEN  Auto
  THEN  (Assert  real-fun(g;a;b)  BY
                          (BLemma  `interval-fun-real-fun`  THEN  Auto)))

---

Home Index