Nuprl Lemma : decidable__equal_equipollent
∀[T:Type]. ∀k:ℕ. (T ~ ℕk ⇒ (∀a,b:T. Dec(a = b ∈ T)))
Proof
Definitions occuring in Statement :
equipollent: A ~ B,
int_seg: {i..j-},
nat: ℕ,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
equipollent: A ~ B,
exists: ∃x:A. B[x],
member: t ∈ T,
nat: ℕ,
decidable: Dec(P),
or: P ∨ Q,
prop: ℙ,
not: ¬A,
false: False,
and: P ∧ Q,
guard: {T},
biject: Bij(A;B;f),
inject: Inj(A;B;f)
Lemmas referenced :
decidable__equal_int_seg,
not_wf,
equal_wf,
and_wf,
equipollent_wf,
int_seg_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
cut,
introduction,
extract_by_obid,
dependent_functionElimination,
natural_numberEquality,
setElimination,
rename,
because_Cache,
hypothesis,
applyEquality,
functionExtensionality,
hypothesisEquality,
cumulativity,
unionElimination,
inlFormation,
isectElimination,
inrFormation,
independent_functionElimination,
equalitySymmetry,
dependent_set_memberEquality,
independent_pairFormation,
applyLambdaEquality,
voidElimination,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}k:\mBbbN{}. (T \msim{} \mBbbN{}k {}\mRightarrow{} (\mforall{}a,b:T. Dec(a = b)))
Date html generated:
2017_09_29-PM-06_04_48
Last ObjectModification:
2017_07_05-PM-06_15_15
Theory : equipollence!!cardinality!
Home
Index