### 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