Nuprl Lemma : not-not-finite-xmiddle
∀[T:Type]. (finite(T) ⇒ (∀P:T ⟶ ℙ. (¬¬(∀i:T. (P[i] ∨ (¬P[i]))))))
Proof
Definitions occuring in Statement :
finite: finite(T),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
finite: finite(T),
exists: ∃x:A. B[x],
nat: ℕ,
prop: ℙ,
equipollent: A ~ B,
biject: Bij(A;B;f),
and: P ∧ Q
Lemmas referenced :
not-not-finite-xmiddle-1,
int_seg_wf,
surject_wf,
finite_wf,
istype-universe,
equipollent_inversion
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
lambdaFormation_alt,
independent_functionElimination,
productElimination,
dependent_pairFormation_alt,
sqequalRule,
productIsType,
functionIsType,
universeIsType,
natural_numberEquality,
setElimination,
rename,
because_Cache,
instantiate,
universeEquality
Latex:
\mforall{}[T:Type]. (finite(T) {}\mRightarrow{} (\mforall{}P:T {}\mrightarrow{} \mBbbP{}. (\mneg{}\mneg{}(\mforall{}i:T. (P[i] \mvee{} (\mneg{}P[i]))))))
Date html generated:
2020_05_19-PM-10_00_48
Last ObjectModification:
2019_10_24-AM-10_45_45
Theory : equipollence!!cardinality!
Home
Index