---

Step * of Lemma subtype_rel_unordered-combination

∀[A,B:Type].  ∀n:ℕ. UnorderedCombination(n;A) ⊆r UnorderedCombination(n;B) supposing strong-subtype(A;B)
BY
{ ((UnivCD THENA Auto) THEN (D 0 THENA Auto) THEN RepeatFor 2 (D -1) THEN MemTypeCD THEN Auto) }

1
1. A : Type
2. B : Type
3. n : ℕ
4. strong-subtype(A;B)
5. x : bag(A)
6. bag-no-repeats(A;x)
7. #(x) = n ∈ ℤ
⊢ bag-no-repeats(B;x)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}n:\mBbbN{}.  UnorderedCombination(n;A)  \msubseteq{}r  UnorderedCombination(n;B)  supposing  strong-subtype(A;B)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  MemTypeCD  THEN  Auto)

---

Home Index