Nuprl Definition : transparent-nset
Transparent(K) == (K ⊆r ℕ) ∧ (∀B:ℕ. ((∀k:K. (k ≤ B)) ∨ (∃k:K. B < k)))
Definitions occuring in Statement :
nat: ℕ,
less_than: a < b,
subtype_rel: A ⊆r B,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q
Definitions occuring in definition :
less_than: a < b,
exists: ∃x:A. B[x],
le: A ≤ B,
all: ∀x:A. B[x],
or: P ∨ Q,
nat: ℕ,
subtype_rel: A ⊆r B,
and: P ∧ Q
FDL editor aliases :
transparent-nset
Latex:
Transparent(K) == (K \msubseteq{}r \mBbbN{}) \mwedge{} (\mforall{}B:\mBbbN{}. ((\mforall{}k:K. (k \mleq{} B)) \mvee{} (\mexists{}k:K. B < k)))
Date html generated:
2019_06_20-PM-03_02_04
Last ObjectModification:
2019_06_13-AM-11_37_01
Theory : continuity
Home
Index