---

Step * of Lemma proper-continuous-implies-functional

∀I:Interval. ∀f:I ⟶ℝ.
  (f[x] (proper)continuous for x ∈ I ⇒ iproper(I) ⇒ (∀a,b:{x:ℝ| x ∈ I} .  ((a = b) ⇒ (f[a] = f[b]))))
BY
{ xxx(Auto THEN Assert ⌜∃m:ℕ+. (icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m)) ∧ (a ∈ i-approx(I;m)))⌝⋅)xxx }

1
.....assertion..... 
1. I : Interval
2. f : I ⟶ℝ
3. f[x] (proper)continuous for x ∈ I
4. iproper(I)
5. a : {x:ℝ| x ∈ I} 
6. b : {x:ℝ| x ∈ I} 
7. a = b
⊢ ∃m:ℕ+. (icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m)) ∧ (a ∈ i-approx(I;m)))

2
1. I : Interval
2. f : I ⟶ℝ
3. f[x] (proper)continuous for x ∈ I
4. iproper(I)
5. a : {x:ℝ| x ∈ I} 
6. b : {x:ℝ| x ∈ I} 
7. a = b
8. ∃m:ℕ+. (icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m)) ∧ (a ∈ i-approx(I;m)))
⊢ f[a] = f[b]

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    (f[x]  (proper)continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  iproper(I)
    {}\mRightarrow{}  (\mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((a  =  b)  {}\mRightarrow{}  (f[a]  =  f[b]))))


By

---

Latex:
xxx(Auto
        THEN  Assert  \mkleeneopen{}\mexists{}m:\mBbbN{}\msupplus{}.  (icompact(i-approx(I;m))  \mwedge{}  iproper(i-approx(I;m))  \mwedge{}  (a  \mmember{}  i-approx(I;m)))\mkleeneclose{}\mcdot{}
        )xxx

---

Home Index