---

Step * of Lemma seq-settype

∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[s:sequence(T)].  s ∈ sequence({x:T| P[x]} ) supposing ∀i:ℕ||s||. (↓P[s[i]])
BY
{ (Auto THEN D -2 THEN RepUR ``seq-len seq-item`` -1 THEN Unfold `sequence` 0 THEN Auto THEN FunExt THEN Auto) }

1
1. T : Type
2. P : T ⟶ ℙ
3. k : ℕ
4. s1 : ℕk ⟶ T
5. ∀i:ℕk. (↓P[s1 i])
6. x : ℕk
⊢ s1 x ∈ {x:T| P[x]} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[s:sequence(T)].    s  \mmember{}  sequence(\{x:T|  P[x]\}  )  supposing  \mforall{}i:\mBbbN{}||s||.  (\mdownarrow{}P[s[i]]\000C)


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  RepUR  ``seq-len  seq-item``  -1
  THEN  Unfold  `sequence`  0
  THEN  Auto
  THEN  FunExt
  THEN  Auto)

---

Home Index