Nuprl Definition : weakly-decidable-nset
WD(K) == (K ⊆r ℕ) ∧ (∀m,k:K. ∀l:{m..k-}. ((l ∈ K) ∨ (¬(l ∈ K))))
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
not: ¬A,
or: P ∨ Q,
and: P ∧ Q,
member: t ∈ T
Definitions occuring in definition :
member: t ∈ T,
not: ¬A,
or: P ∨ Q,
int_seg: {i..j-},
all: ∀x:A. B[x],
nat: ℕ,
subtype_rel: A ⊆r B,
and: P ∧ Q
FDL editor aliases :
weakly-decidable-nset
Latex:
WD(K) == (K \msubseteq{}r \mBbbN{}) \mwedge{} (\mforall{}m,k:K. \mforall{}l:\{m..k\msupminus{}\}. ((l \mmember{} K) \mvee{} (\mneg{}(l \mmember{} K))))
Date html generated:
2019_06_20-PM-03_01_49
Last ObjectModification:
2019_06_13-PM-00_36_30
Theory : continuity
Home
Index