---

Step * of Lemma classical-exists-implies-approx

No Annotations
∀I:{I:Interval| icompact(I)} . ∀f:{f:I ⟶ℝ| ifun(f;I)} .
  ((¬¬(∃x:{x:ℝ| x ∈ I} . (f[x] = r0))) ⇒ (∀e:{e:ℝ| r0 < e} . ∃x:{x:ℝ| x ∈ I} . (|f[x]| < e)))
BY
{ ((InstLemma `classical-exists-n-implies-approx` [] THEN ParallelLast') THEN (D -1 With ⌜1⌝  THENA Auto)) }

1
1. I : {I:Interval| icompact(I)} 
2. ∀f:{f:I^1 ⟶ ℝ| ∀a,b:I^1.  (req-vec(1;a;b) ⇒ ((f a) = (f b)))} 
     ((¬¬(∃x:I^1. ((f x) = r0))) ⇒ (∀e:{e:ℝ| r0 < e} . ∃x:I^1. (|f x| < e)))
⊢ ∀f:{f:I ⟶ℝ| ifun(f;I)} . ((¬¬(∃x:{x:ℝ| x ∈ I} . (f[x] = r0))) ⇒ (∀e:{e:ℝ| r0 < e} . ∃x:{x:ℝ| x ∈ I} . (|f[x]| < e)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:\{I:Interval|  icompact(I)\}  .  \mforall{}f:\{f:I  {}\mrightarrow{}\mBbbR{}|  ifun(f;I)\}  .
    ((\mneg{}\mneg{}(\mexists{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[x]  =  r0)))  {}\mRightarrow{}  (\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .  \mexists{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (|f[x]|  <  e)))


By

---

Latex:
((InstLemma  `classical-exists-n-implies-approx`  []  THEN  ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto)
  )

---

Home Index