---

Step * 1 1 1 of Lemma Spread-family-ext


1. P : Type
2. Pos : Type
3. f : Pos ⟶ ℤ
4. Mv : ℤ ⟶ P ⟶ P ⟶ Type
5. X : ℕ ⟶ P ⟶ Type
6. p : P
7. x : ⋂n:ℕ. (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (X n q)))
8. x ~ <fst(x), snd(x)>
9. fst(x) ∈ Pos
⊢ snd(x) ∈ q:P ⟶ Mv[f (fst(x));p;q] ⟶ (⋂n:ℕ. (X n q))
BY
{ (ExtWith [`a'] [⌜Top⌝]⋅⋅ THEN Auto THEN ExtWith [`b'] [⌜Top⌝]⋅⋅ THEN Auto)⋅ }

1
1. P : Type
2. Pos : Type
3. f : Pos ⟶ ℤ
4. Mv : ℤ ⟶ P ⟶ P ⟶ Type
5. X : ℕ ⟶ P ⟶ Type
6. p : P
7. x : ⋂n:ℕ. (a:Pos × (q:P ⟶ Mv[f a;p;q] ⟶ (X n q)))
8. x ~ <fst(x), snd(x)>
9. fst(x) ∈ Pos
10. a : P
11. b : Mv[f (fst(x));p;a]
12. n : ℕ
⊢ (snd(x)) a b ∈ X n a

---

Latex:

---

Latex:

1.  P  :  Type
2.  Pos  :  Type
3.  f  :  Pos  {}\mrightarrow{}  \mBbbZ{}
4.  Mv  :  \mBbbZ{}  {}\mrightarrow{}  P  {}\mrightarrow{}  P  {}\mrightarrow{}  Type
5.  X  :  \mBbbN{}  {}\mrightarrow{}  P  {}\mrightarrow{}  Type
6.  p  :  P
7.  x  :  \mcap{}n:\mBbbN{}.  (a:Pos  \mtimes{}  (q:P  {}\mrightarrow{}  Mv[f  a;p;q]  {}\mrightarrow{}  (X  n  q)))
8.  x  \msim{}  <fst(x),  snd(x)>
9.  fst(x)  \mmember{}  Pos
\mvdash{}  snd(x)  \mmember{}  q:P  {}\mrightarrow{}  Mv[f  (fst(x));p;q]  {}\mrightarrow{}  (\mcap{}n:\mBbbN{}.  (X  n  q))


By

---

Latex:
(ExtWith  [`a']  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}\mcdot{}  THEN  Auto  THEN  ExtWith  [`b']  [\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index