Nuprl Definition : absolutelyfree
absolutelyfree{i:l}(T) ==
((T ⊆r (ℕ ⟶ ℕ)) ∧ (∀P:T ⟶ ℙ. ∀f:T. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:T. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))))
∧ (∀S:Type
((S ⊆r (ℕ ⟶ ℕ)) ⇒ (∀P:S ⟶ ℙ. ∀f:S. ((P f) ⇒ ⇃(∃k:ℕ. ∀g:S. ((f = g ∈ (ℕk ⟶ ℕ)) ⇒ (P g))))) ⇒ (S ⊆r T)))
Definitions occuring in Statement :
quotient: x,y:A//B[x; y],
int_seg: {i..j-},
nat: ℕ,
subtype_rel: A ⊆r B,
prop: ℙ,
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,
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
universe: Type,
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,
subtype_rel: A ⊆r B
FDL editor aliases :
absolutelyfree
Latex:
absolutelyfree\{i:l\}(T) ==
((T \msubseteq{}r (\mBbbN{} {}\mrightarrow{} \mBbbN{})) \mwedge{} (\mforall{}P:T {}\mrightarrow{} \mBbbP{}. \mforall{}f:T. ((P f) {}\mRightarrow{} \00D9(\mexists{}k:\mBbbN{}. \mforall{}g:T. ((f = g) {}\mRightarrow{} (P g))))))
\mwedge{} (\mforall{}S:Type
((S \msubseteq{}r (\mBbbN{} {}\mrightarrow{} \mBbbN{}))
{}\mRightarrow{} (\mforall{}P:S {}\mrightarrow{} \mBbbP{}. \mforall{}f:S. ((P f) {}\mRightarrow{} \00D9(\mexists{}k:\mBbbN{}. \mforall{}g:S. ((f = g) {}\mRightarrow{} (P g)))))
{}\mRightarrow{} (S \msubseteq{}r T)))
Date html generated:
2017_09_29-PM-06_10_29
Last ObjectModification:
2017_04_21-PM-00_34_46
Theory : continuity
Home
Index