---

Step * of Lemma combination_functionality

∀[A,B:Type].  ∀n,m:ℤ.  (A ~ B ⇒ Combination(n;A) ~ Combination(m;B) supposing n = m ∈ ℤ)
BY
{ xxx((Auto THEN D -2) THEN With ⌜λL.map(f;L)⌝ (D 0)⋅ THEN Auto THEN HypSubst' -1 0 THEN ThinVar `n')xxx }

1
1. [A] : Type
2. [B] : Type
3. m : ℤ
4. f : A ⟶ B
5. Bij(A;B;f)
⊢ Bij(Combination(m;A);Combination(m;B);λL.map(f;L))

---

Latex:

---

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


By

---

Latex:
xxx((Auto  THEN  D  -2)
        THEN  With  \mkleeneopen{}\mlambda{}L.map(f;L)\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto
        THEN  HypSubst'  -1  0
        THEN  ThinVar  `n')xxx

---

Home Index