---

Step * 1 1 of Lemma append_segment


1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
5. k : {j...||as||}
⊢ ((Π i ≤ k < j. [as[k]]) @ (Π j ≤ k < k. [as[k]])) = (Π i ≤ k < k. [as[k]]) ∈ (T List)
BY
{ (RWN 3 (LemmaWithC [`b',j] `mon_itop_split`) 0 THENA Auto) }

1
1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
5. k : {j...||as||}
⊢ ((Π i ≤ k < j. [as[k]]) @ (Π j ≤ k < k. [as[k]])) = ((Π i ≤ k < j. [as[k]]) * (Π j ≤ k < k. [as[k]])) ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  i  :  \{0...||as||\}
4.  j  :  \{i...||as||\}
5.  k  :  \{j...||as||\}
\mvdash{}  ((\mPi{}  i  \mleq{}  k  <  j.  [as[k]])  @  (\mPi{}  j  \mleq{}  k  <  k.  [as[k]]))  =  (\mPi{}  i  \mleq{}  k  <  k.  [as[k]])


By

---

Latex:
(RWN  3  (LemmaWithC  [`b',j]  `mon\_itop\_split`)  0  THENA  Auto)

---

Home Index