### Nuprl Lemma : combination_functionality

`∀[A,B:Type].  ∀n,m:ℤ.  (A ~ B `` Combination(n;A) ~ Combination(m;B) supposing n = m ∈ ℤ)`

Proof

Definitions occuring in Statement :  combination: `Combination(n;T)` equipollent: `A ~ B` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  prop: `ℙ` guard: `{T}` sq_type: `SQType(T)` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]` equipollent: `A ~ B` member: `t ∈ T` uimplies: `b supposing a` implies: `P `` Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` biject: `Bij(A;B;f)` and: `P ∧ Q` surject: `Surj(A;B;f)` inject: `Inj(A;B;f)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` true: `True` squash: `↓T` compose: `f o g` top: `Top` combination: `Combination(n;T)`
Lemmas referenced :  equipollent_wf equal-wf-base biject_wf int_subtype_base subtype_base_sq subtype_rel_wf combination_wf subtype_rel_self map_wf_combination biject-inverse equal_wf list_wf iff_weakening_equal true_wf squash_wf map_wf map-map top_wf subtype_rel_list map-id length_wf equal-wf-T-base no_repeats_wf
Rules used in proof :  universeEquality independent_functionElimination dependent_functionElimination intEquality instantiate sqequalRule applyLambdaEquality equalitySymmetry hyp_replacement independent_isectElimination because_Cache applyEquality functionExtensionality hypothesisEquality cumulativity isectElimination extract_by_obid lambdaEquality dependent_pairFormation productElimination sqequalHypSubstitution rename thin hypothesis axiomEquality introduction cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution independent_pairFormation baseClosed imageMemberEquality natural_numberEquality equalityTransitivity imageElimination voidEquality voidElimination isect_memberEquality setElimination productEquality dependent_set_memberEquality

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

Date html generated: 2018_05_21-PM-08_08_13
Last ObjectModification: 2017_12_07-PM-06_24_23

Theory : general

Home Index