Nuprl Definition : unsquashed-WCP
unsquashed-WCP ==
∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀a,b:ℕ ⟶ ℕ. ((∀i:ℕM a. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
equal: s = t ∈ T,
nat: ℕ,
apply: f a
FDL editor aliases :
unsquashed-WCP
Latex:
unsquashed-WCP ==
\mforall{}F:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mexists{}M:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}. \mforall{}a,b:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((\mforall{}i:\mBbbN{}M a. ((a i) = (b i))) {}\mRightarrow{} ((F a) = (F b)))
Date html generated:
2016_05_14-PM-04_14_52
Last ObjectModification:
2015_09_22-PM-06_02_26
Theory : fan-theorem
Home
Index