Nuprl Lemma : equipollent-partition
∀k:ℕ
∀[A:Type]
(A ~ ℕk
⇒ (∀[P:A ⟶ ℙ]. ((∀x:A. Dec(P[x])) ⇒ (∃i,j:ℕ. ((k = (i + j) ∈ ℤ) ∧ {a:A| P[a]} ~ ℕi ∧ {a:A| ¬P[a]} ~ ℕj)))))
Proof
Definitions occuring in Statement :
equipollent: A ~ B,
int_seg: {i..j-},
nat: ℕ,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
exists: ∃x:A. B[x],
decidable: Dec(P),
or: P ∨ Q,
isl: isl(x),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
cand: A c∧ B,
rev_implies: P ⇐ Q,
true: True,
bfalse: ff,
false: False,
not: ¬A,
so_apply: x[s],
subtype_rel: A ⊆r B,
prop: ℙ,
nat: ℕ,
so_lambda: λ2x.t[x],
uimplies: b supposing a,
squash: ↓T,
guard: {T},
uiff: uiff(P;Q),
sq_stable: SqStable(P),
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
equipollent-iff-list,
btrue_wf,
istype-true,
bfalse_wf,
istype-void,
subtype_rel_self,
decidable_wf,
equipollent_wf,
int_seg_wf,
istype-universe,
istype-nat,
length_wf_nat,
filter_wf5,
l_member_wf,
bnot_wf,
set_subtype_base,
le_wf,
int_subtype_base,
length_wf,
not_wf,
equal_wf,
squash_wf,
true_wf,
filter-split-length,
iff_weakening_equal,
filter_type,
subtype_rel_list,
assert_wf,
subtype_rel_sets_simple,
istype-assert,
no_repeats_wf,
no_repeats-settype,
no_repeats_filter,
l_member-settype,
member_filter,
sq_stable_from_decidable,
decidable__assert,
assert_of_bnot,
subtype_rel_list_set
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
dependent_functionElimination,
productElimination,
independent_functionElimination,
hypothesis,
rename,
applyEquality,
functionExtensionality,
inhabitedIsType,
unionElimination,
sqequalRule,
independent_pairFormation,
natural_numberEquality,
voidElimination,
universeIsType,
instantiate,
universeEquality,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
because_Cache,
functionIsType,
setElimination,
dependent_pairFormation_alt,
lambdaEquality_alt,
setIsType,
productIsType,
intEquality,
independent_isectElimination,
addEquality,
sqequalBase,
setEquality,
baseApply,
closedConclusion,
baseClosed,
imageElimination,
imageMemberEquality,
hyp_replacement,
applyLambdaEquality
Latex:
\mforall{}k:\mBbbN{}
\mforall{}[A:Type]
(A \msim{} \mBbbN{}k
{}\mRightarrow{} (\mforall{}[P:A {}\mrightarrow{} \mBbbP{}]
((\mforall{}x:A. Dec(P[x])) {}\mRightarrow{} (\mexists{}i,j:\mBbbN{}. ((k = (i + j)) \mwedge{} \{a:A| P[a]\} \msim{} \mBbbN{}i \mwedge{} \{a:A| \mneg{}P[a]\} \msim{} \mBbbN{}j))))\000C)
Date html generated:
2020_05_19-PM-10_00_34
Last ObjectModification:
2020_01_04-PM-08_00_14
Theory : equipollence!!cardinality!
Home
Index