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