---

Step * of Lemma stable_real-vec-be

∀n:ℕ. ∀a,c:ℝ^n.  (a ≠ c ⇒ (∀b:ℝ^n. Stable{real-vec-be(n;a;b;c)}))
BY
{ (Auto THEN Unfold `real-vec-be` 0 THEN (D 0 THENA Auto)) }

1
1. n : ℕ
2. a : ℝ^n
3. c : ℝ^n
4. a ≠ c
5. b : ℝ^n
6. ¬¬(∃t:ℝ. ((t ∈ [r0, r1]) ∧ req-vec(n;b;t*a + r1 - t*c)))
⊢ ∃t:ℝ. ((t ∈ [r0, r1]) ∧ req-vec(n;b;t*a + r1 - t*c))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,c:\mBbbR{}\^{}n.    (a  \mneq{}  c  {}\mRightarrow{}  (\mforall{}b:\mBbbR{}\^{}n.  Stable\{real-vec-be(n;a;b;c)\}))


By

---

Latex:
(Auto  THEN  Unfold  `real-vec-be`  0  THEN  (D  0  THENA  Auto))

---

Home Index