Nuprl Definition : squashed-continuity1-rel
squashed-continuity1-rel(A) ==
(∀a:ℕ ⟶ ℕ. ⇃(∃b:ℕ ⟶ ℕ. (A a b))) ⟶ ⇃(∃c:(ℕ ⟶ ℕ) ⟶ ℕ
((∀a:ℕ ⟶ ℕ
⇃(∃n:ℕ. ∀b:ℕ ⟶ ℕ. ((a = b ∈ (ℕn ⟶ ℕ)) ⇒ ((c a) = (c b) ∈ ℕ))))
∧ (∀a:ℕ ⟶ ℕ. (A a shift-seq(c;a)))))
Definitions occuring in Statement :
shift-seq: shift-seq(c;a),
quotient: x,y:A//B[x; y],
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
true: True,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
true: True,
shift-seq: shift-seq(c;a),
apply: f a,
nat: ℕ,
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
equal: s = t ∈ T,
natural_number: $n,
int_seg: {i..j-},
implies: P ⇒ Q,
exists: ∃x:A. B[x],
quotient: x,y:A//B[x; y],
and: P ∧ Q
FDL editor aliases :
squashed-continuity1-rel
Latex:
squashed-continuity1-rel(A) ==
(\mforall{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \00D9(\mexists{}b:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (A a b))) {}\mrightarrow{} \00D9(\mexists{}c:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} \mBbbN{}
((\mforall{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{}
\00D9(\mexists{}n:\mBbbN{}. \mforall{}b:\mBbbN{} {}\mrightarrow{} \mBbbN{}. ((a = b) {}\mRightarrow{} ((c a) = (c b)))))
\mwedge{} (\mforall{}a:\mBbbN{} {}\mrightarrow{} \mBbbN{}. (A a shift-seq(c;a)))))
Date html generated:
2017_04_20-AM-07_35_40
Last ObjectModification:
2017_04_07-PM-05_56_17
Theory : continuity
Home
Index