---

Step * of Lemma l_all_exists_injection

∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ]. ∀[P:B ⟶ ℙ].
  ∀L:A List
    ((∀x∈L.∃y:B. (R[x;y] ∧ P[y])) ⇒ (∃f:ℕ||L|| ⟶ {y:B| P[y]} . Inj(ℕ||L||;{y:B| P[y]} ;f))) supposing 
       (no_repeats(A;L) and 
       (∀x1,x2:A. ∀y:B.  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ A))))
BY
{ (Auto THEN Unfold `l_all` -1) }

1
1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ B ⟶ ℙ
4. [P] : B ⟶ ℙ
5. L : A List
6. ∀x1,x2:A. ∀y:B.  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ A))
7. no_repeats(A;L)
8. ∀i:ℕ||L||. ∃y:B. (R[L[i];y] ∧ P[y])
⊢ ∃f:ℕ||L|| ⟶ {y:B| P[y]} . Inj(ℕ||L||;{y:B| P[y]} ;f)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:B  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}L:A  List
        ((\mforall{}x\mmember{}L.\mexists{}y:B.  (R[x;y]  \mwedge{}  P[y]))  {}\mRightarrow{}  (\mexists{}f:\mBbbN{}||L||  {}\mrightarrow{}  \{y:B|  P[y]\}  .  Inj(\mBbbN{}||L||;\{y:B|  P[y]\}  ;f)))  suppos\000Cing 
              (no\_repeats(A;L)  and 
              (\mforall{}x1,x2:A.  \mforall{}y:B.    (R[x1;y]  {}\mRightarrow{}  R[x2;y]  {}\mRightarrow{}  (x1  =  x2))))


By

---

Latex:
(Auto  THEN  Unfold  `l\_all`  -1)

---

Home Index