Nuprl Definition : type-continuous'
semi-continuous(λT.F[T]) == ∀[X:type-incr-chain{i:l}()]. (F[⋃n:ℕ.(X n)] ⊆r ⋃n:ℕ.F[X n])
Definitions occuring in Statement :
type-incr-chain: type-incr-chain{i:l}(),
nat: ℕ,
subtype_rel: A ⊆r B,
tunion: ⋃x:A.B[x],
uall: ∀[x:A]. B[x],
apply: f a
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
type-incr-chain: type-incr-chain{i:l}(),
subtype_rel: A ⊆r B,
tunion: ⋃x:A.B[x],
nat: ℕ,
apply: f a
FDL editor aliases :
type-continuous'
Latex:
semi-continuous(\mlambda{}T.F[T]) == \mforall{}[X:type-incr-chain\{i:l\}()]. (F[\mcup{}n:\mBbbN{}.(X n)] \msubseteq{}r \mcup{}n:\mBbbN{}.F[X n])
Date html generated:
2016_05_15-PM-06_52_16
Last ObjectModification:
2015_09_23-AM-08_07_11
Theory : general
Home
Index