Nuprl Lemma : markov-streamless-product
(∀P:ℕ ⟶ ℙ. ((∀m:ℕ. ((P m) ∨ (¬(P m)))) ⇒ (¬(∀m:ℕ. (¬(P m)))) ⇒ (∃m:ℕ. (P m))))
⇒ (∀A,B:Type. (streamless(A) ⇒ streamless(B) ⇒ streamless(A × B)))
Proof
Definitions occuring in Statement :
streamless: streamless(T),
nat: ℕ,
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
implies: P ⇒ Q,
all: ∀x:A. B[x],
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
cand: A c∧ B,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ,
or: P ∨ Q,
subtype_rel: A ⊆r B,
not: ¬A,
false: False,
exists: ∃x:A. B[x],
nat: ℕ
Lemmas referenced :
markov-streamless-iff,
decidable__equal_product,
istype-universe,
streamless_wf,
nat_wf,
subtype_rel_self,
istype-void,
equipollent_wf,
int_seg_wf,
mul_bounds_1a,
le_wf,
equipollent_same,
equipollent_functionality_wrt_equipollent,
product_functionality_wrt_equipollent,
equipollent_inversion,
equipollent-multiply
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
independent_functionElimination,
thin,
hypothesis,
dependent_functionElimination,
hypothesisEquality,
productElimination,
productEquality,
isectElimination,
sqequalRule,
lambdaEquality_alt,
inhabitedIsType,
productIsType,
independent_pairFormation,
universeIsType,
universeEquality,
functionIsType,
unionIsType,
applyEquality,
instantiate,
because_Cache,
voidElimination,
natural_numberEquality,
setElimination,
rename,
dependent_pairFormation_alt,
dependent_set_memberEquality_alt,
multiplyEquality
Latex:
(\mforall{}P:\mBbbN{} {}\mrightarrow{} \mBbbP{}. ((\mforall{}m:\mBbbN{}. ((P m) \mvee{} (\mneg{}(P m)))) {}\mRightarrow{} (\mneg{}(\mforall{}m:\mBbbN{}. (\mneg{}(P m)))) {}\mRightarrow{} (\mexists{}m:\mBbbN{}. (P m))))
{}\mRightarrow{} (\mforall{}A,B:Type. (streamless(A) {}\mRightarrow{} streamless(B) {}\mRightarrow{} streamless(A \mtimes{} B)))
Date html generated:
2019_10_15-AM-11_35_42
Last ObjectModification:
2018_10_09-AM-10_56_39
Theory : general
Home
Index