---

Step * 2 of Lemma real-vec-extend_wf_interval


1. I : Interval
2. k : ℕ
3. a : ℝ^k
4. ∀i:ℕk. (a i ∈ I)
5. z : ℝ
6. z ∈ I
7. i : ℕk + 1@i
⊢ a++z i ∈ I
BY
{ (RepUR ``real-vec-extend`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  k  :  \mBbbN{}
3.  a  :  \mBbbR{}\^{}k
4.  \mforall{}i:\mBbbN{}k.  (a  i  \mmember{}  I)
5.  z  :  \mBbbR{}
6.  z  \mmember{}  I
7.  i  :  \mBbbN{}k  +  1@i
\mvdash{}  a++z  i  \mmember{}  I


By

---

Latex:
(RepUR  ``real-vec-extend``  0  THEN  AutoSplit)

---

Home Index