---

Step * of Lemma const-nonzero-on

∀[I:Interval]. ∀a:ℝ. (a ≠ r0 ⇒ a≠r0 for x ∈ I)
BY
{ ((Auto THEN D 0 THEN Auto) THEN With ⌜|a|⌝ (D 0)⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}a:\mBbbR{}.  (a  \mneq{}  r0  {}\mRightarrow{}  a\mneq{}r0  for  x  \mmember{}  I)


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)  THEN  With  \mkleeneopen{}|a|\mkleeneclose{}  (D  0)\mcdot{}  THEN  EAuto  1)

---

Home Index