Nuprl Definition : base-CP
base-CP() ==
∀F:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ ⋂ Base
∃M:ℕ ⟶ ℕ ⋂ Base ⟶ ℕ. ∀a,b:ℕ ⟶ ℕ ⋂ Base. ((∀i:ℕM a. ((a i) = (b i) ∈ ℕ)) ⇒ ((F a) = (F b) ∈ ℕ))
Definitions occuring in Statement :
isect2: T1 ⋂ T2,
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,
base: Base,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
isect2: T1 ⋂ T2,
function: x:A ⟶ B[x],
base: Base,
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 :
base-CP
Latex:
base-CP() ==
\mforall{}F:\mBbbN{} {}\mrightarrow{} \mBbbN{} \mcap{} Base {}\mrightarrow{} \mBbbN{} \mcap{} Base
\mexists{}M:\mBbbN{} {}\mrightarrow{} \mBbbN{} \mcap{} Base {}\mrightarrow{} \mBbbN{}. \mforall{}a,b:\mBbbN{} {}\mrightarrow{} \mBbbN{} \mcap{} Base. ((\mforall{}i:\mBbbN{}M a. ((a i) = (b i))) {}\mRightarrow{} ((F a) = (F b)))
Date html generated:
2016_05_14-PM-04_14_57
Last ObjectModification:
2015_09_22-PM-06_02_30
Theory : fan-theorem
Home
Index