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