### Nuprl Definition : is-absolutely-free

`is-absolutely-free{i:l}(f) ==  ∀P:(ℕ ⟶ ℕ) ⟶ ℙ. ((P f) `` ⇃(∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((f = g ∈ (ℕk ⟶ ℕ)) `` (P g))))`

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` int_seg: `{i..j-}` nat: `ℕ` prop: `ℙ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` true: `True` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions occuring in definition :  prop: `ℙ` quotient: `x,y:A//B[x; y]` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` equal: `s = t ∈ T` function: `x:A ⟶ B[x]` int_seg: `{i..j-}` natural_number: `\$n` nat: `ℕ` apply: `f a` true: `True`
FDL editor aliases :  is-absolutely-free

Latex:
is-absolutely-free\{i:l\}(f)  ==    \mforall{}P:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  ((P  f)  {}\mRightarrow{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  =  g)  {}\mRightarrow{}  (P  g))))

Date html generated: 2017_09_29-PM-06_09_13
Last ObjectModification: 2017_04_22-PM-05_23_35

Theory : continuity

Home Index