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