### Nuprl Lemma : subtype_rel_unordered-combination

`∀[A,B:Type].  ∀n:ℕ. UnorderedCombination(n;A) ⊆r UnorderedCombination(n;B) supposing strong-subtype(A;B)`

Proof

Definitions occuring in Statement :  unordered-combination: `UnorderedCombination(n;T)` strong-subtype: `strong-subtype(A;B)` nat: `ℕ` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` unordered-combination: `UnorderedCombination(n;T)` and: `P ∧ Q` strong-subtype: `strong-subtype(A;B)` cand: `A c∧ B` prop: `ℙ` nat: `ℕ` bag-no-repeats: `bag-no-repeats(T;bs)` squash: `↓T` exists: `∃x:A. B[x]` guard: `{T}` implies: `P `` Q`
Lemmas referenced :  subtype_rel_bag bag-no-repeats_wf equal_wf bag-size_wf nat_wf unordered-combination_wf strong-subtype_wf subtype_rel_list bag_wf list-subtype-bag no_repeats_wf equal_functionality_wrt_subtype_rel2 no_repeats-strong-subtype
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lambdaEquality sqequalHypSubstitution setElimination thin rename productElimination dependent_set_memberEquality hypothesisEquality applyEquality extract_by_obid isectElimination independent_isectElimination hypothesis sqequalRule independent_pairFormation productEquality cumulativity intEquality axiomEquality dependent_functionElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality imageElimination dependent_pairFormation imageMemberEquality baseClosed independent_functionElimination

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

Date html generated: 2017_10_01-AM-09_05_34
Last ObjectModification: 2017_07_26-PM-04_45_45

Theory : bags

Home Index