---

Step * of Lemma product-map

∀[A,B,C:Type].
  ∀as:A List. ∀bs:B List. ∀F:A ⟶ B ⟶ C.  ∃cs:C List. ∀c:C. ((c ∈ cs) ⇐⇒ (∃a∈as. (∃b∈bs. c = (F a b) ∈ C)))
BY
{ xxx((UnivCD THENA Auto)
      THEN (With ⌜product-map(F;as;bs)⌝ (D 0)⋅ THENA Auto)
      THEN (D 0 THENA Auto)
      THEN RWW "member-product-map l_exists_iff" 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].
    \mforall{}as:A  List.  \mforall{}bs:B  List.  \mforall{}F:A  {}\mrightarrow{}  B  {}\mrightarrow{}  C.
        \mexists{}cs:C  List.  \mforall{}c:C.  ((c  \mmember{}  cs)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}a\mmember{}as.  (\mexists{}b\mmember{}bs.  c  =  (F  a  b))))


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  (With  \mkleeneopen{}product-map(F;as;bs)\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
        THEN  (D  0  THENA  Auto)
        THEN  RWW  "member-product-map  l\_exists\_iff"  0
        THEN  Auto)xxx

---

Home Index