---

Step * of Lemma rel_finite-restrict

∀[E:Type]. ∀P:E ⟶ 𝔹. ∀[R:E ⟶ E ⟶ ℙ]. (rel_finite(E;R) ⇒ rel_finite({e:E| ↑(P e)} ;R))
BY
{ ((Auto THEN D 0 THEN Auto)
   THEN (With ⌜x⌝ (D (-2))⋅ THENA Auto)
   THEN ExRepD
   THEN With ⌜filter(P;L)⌝ (D 0)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}P:E  {}\mrightarrow{}  \mBbbB{}.  \mforall{}[R:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  (rel\_finite(E;R)  {}\mRightarrow{}  rel\_finite(\{e:E|  \muparrow{}(P  e)\}  ;R))


By

---

Latex:
((Auto  THEN  D  0  THEN  Auto)
  THEN  (With  \mkleeneopen{}x\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  With  \mkleeneopen{}filter(P;L)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index