Step * of Lemma subtype_rel_unordered-combination

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

1
1. Type
2. Type
3. : ℕ
4. strong-subtype(A;B)
5. 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