---

Step * of Lemma unordered-combination_functionality

∀[A,B:Type].  ∀n,m:ℕ.  (A ~ B ⇒ UnorderedCombination(n;A) ~ UnorderedCombination(m;B) supposing n = m ∈ ℤ)
BY
{ ((Auto THEN D -2)
   THEN Assert ⌜∀[A,B:Type].
                  ∀f:A ⟶ B
                    (Inj(A;B;f) ⇒ (∀n:ℕ. ∀b:UnorderedCombination(n;A).  (bag-map(f;b) ∈ UnorderedCombination(n;B))))⌝⋅
   ) }

1
.....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))))

2
1. [A] : Type
2. [B] : Type
3. n : ℕ
4. m : ℕ
5. f : A ⟶ B
6. Bij(A;B;f)
7. n = m ∈ ℤ
8. ∀[A,B:Type].
     ∀f:A ⟶ B. (Inj(A;B;f) ⇒ (∀n:ℕ. ∀b:UnorderedCombination(n;A).  (bag-map(f;b) ∈ UnorderedCombination(n;B))))
⊢ UnorderedCombination(n;A) ~ UnorderedCombination(m;B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}n,m:\mBbbN{}.    (A  \msim{}  B  {}\mRightarrow{}  UnorderedCombination(n;A)  \msim{}  UnorderedCombination(m;B)  supposing  n  =  m)


By

---

Latex:
((Auto  THEN  D  -2)
  THEN  Assert  \mkleeneopen{}\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))))\mkleeneclose{}\mcdot{}
  )

---

Home Index