---

Step * of Lemma sublevelset-closed

∀I:Interval. ∀[f:I ⟶ℝ]. ∀[c:ℝ].  (i-closed(I) ⇒ f(x) continuous for x ∈ I ⇒ closed-rset(sublevelset(I;f;c)))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN D -1
   THEN RepUR ``sublevelset`` 0
   THEN D -1
   THEN RepUR ``sublevelset`` -1
   THEN InstLemma `i-closed-closed` [⌜I⌝]⋅
   THEN Auto) }

1
1. I : Interval@i
2. [f] : I ⟶ℝ
3. [c] : ℝ
4. i-closed(I)@i
5. f(x) continuous for x ∈ I@i
6. y : ℝ@i
7. x : ℕ ⟶ ℝ@i
8. lim n→∞.x[n] = y@i
9. ∀n:ℕ. ((x[n] ∈ I) ∧ (f(x[n]) ≤ c))@i
10. closed-rset(λx.(x ∈ I))
⊢ y ∈ I

2
1. I : Interval@i
2. [f] : I ⟶ℝ
3. [c] : ℝ
4. i-closed(I)@i
5. f(x) continuous for x ∈ I@i
6. y : ℝ@i
7. x : ℕ ⟶ ℝ@i
8. lim n→∞.x[n] = y@i
9. ∀n:ℕ. ((x[n] ∈ I) ∧ (f(x[n]) ≤ c))@i
10. closed-rset(λx.(x ∈ I))
11. y ∈ I
⊢ f(y) ≤ c

---

Latex:

---

Latex:
\mforall{}I:Interval
    \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].  \mforall{}[c:\mBbbR{}].    (i-closed(I)  {}\mRightarrow{}  f(x)  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  closed-rset(sublevelset(I;f;c)))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  D  -1
  THEN  RepUR  ``sublevelset``  0
  THEN  D  -1
  THEN  RepUR  ``sublevelset``  -1
  THEN  InstLemma  `i-closed-closed`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index