---

Step * 1 of Lemma W-uwellfounded_witness


1. A : Type
2. B : A ⟶ Type
3. P : W(A;a.B[a]) ⟶ ℙ
4. f : ⋂j:W(A;a.B[a]). ((⋂k:{k:W(A;a.B[a])| k <  j} . P[k]) ⇒ P[j])
⊢ ∀w:W(A;a.B[a]). (fix(f) ∈ P[w])
BY
{ WInd }

1
1. A : Type
2. B : A ⟶ Type
3. P : W(A;a.B[a]) ⟶ ℙ
4. f : ⋂j:W(A;a.B[a]). ((⋂k:{k:W(A;a.B[a])| k <  j} . P[k]) ⇒ P[j])
5. a : A
6. f1 : B[a] ⟶ W(A;a.B[a])
7. ∀w:W(A;a.B[a]). ((w <  Wsup(a;f1)) ⇒ (fix(f) ∈ P[w]))
⊢ ∀w:W(A;a.B[a]). ∀v:w ≤  Wsup(a;f1).  (fix(f) ∈ P[w])

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  P  :  W(A;a.B[a])  {}\mrightarrow{}  \mBbbP{}
4.  f  :  \mcap{}j:W(A;a.B[a]).  ((\mcap{}k:\{k:W(A;a.B[a])|  k  <    j\}  .  P[k])  {}\mRightarrow{}  P[j])
\mvdash{}  \mforall{}w:W(A;a.B[a]).  (fix(f)  \mmember{}  P[w])


By

---

Latex:
WInd

---

Home Index