---

Step * 1 of Lemma unordered-combination_functionality

.....assertion..... 
1. [A] : Type
2. [B] : Type
3. n : ℕ
4. m : ℕ
5. f : A ⟶ B
6. Bij(A;B;f)
7. n = m ∈ ℤ
⊢ ∀[A,B:Type].
    ∀f:A ⟶ B. (Inj(A;B;f) ⇒ (∀n:ℕ. ∀b:UnorderedCombination(n;A).  (bag-map(f;b) ∈ UnorderedCombination(n;B))))
BY
{ (Auto
   THEN D (-1)
   THEN MemTypeD 0
   THEN Auto
   THEN RWW "bag-size-map" 0
   THEN Auto
   THEN BLemma `bag-map-no-repeats`
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  Type
2.  [B]  :  Type
3.  n  :  \mBbbN{}
4.  m  :  \mBbbN{}
5.  f  :  A  {}\mrightarrow{}  B
6.  Bij(A;B;f)
7.  n  =  m
\mvdash{}  \mforall{}[A,B:Type].
        \mforall{}f:A  {}\mrightarrow{}  B
            (Inj(A;B;f)
            {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}b:UnorderedCombination(n;A).    (bag-map(f;b)  \mmember{}  UnorderedCombination(n;B))))


By

---

Latex:
(Auto
  THEN  D  (-1)
  THEN  MemTypeD  0
  THEN  Auto
  THEN  RWW  "bag-size-map"  0
  THEN  Auto
  THEN  BLemma  `bag-map-no-repeats`
  THEN  Auto)

---

Home Index