Nuprl Definition : relclosed-set
closed(x,a.R[x; a])s == ∀x,a:Set{i:l}. ((x ⊆ s) ⇒ R[x; a] ⇒ (a ∈ s))
Definitions occuring in Statement :
setsubset: (a ⊆ b),
setmem: (x ∈ s),
Set: Set{i:l},
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
setmem: (x ∈ s),
implies: P ⇒ Q,
setsubset: (a ⊆ b),
Set: Set{i:l},
all: ∀x:A. B[x]
FDL editor aliases :
relclosed-set
Latex:
closed(x,a.R[x; a])s == \mforall{}x,a:Set\{i:l\}. ((x \msubseteq{} s) {}\mRightarrow{} R[x; a] {}\mRightarrow{} (a \mmember{} s))
Date html generated:
2018_05_29-PM-01_53_19
Last ObjectModification:
2018_05_25-AM-08_29_28
Theory : constructive!set!theory
Home
Index