Nuprl Definition : fset-closure
(c = fs closure of s) == s ⊆ c ∧ (c closed under fs) ∧ (∀c':fset(T). (s ⊆ c' ⇒ (c' closed under fs) ⇒ c ⊆ c'))
Definitions occuring in Statement :
fset-closed: (s closed under fs),
f-subset: xs ⊆ ys,
fset: fset(T),
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
fset: fset(T),
implies: P ⇒ Q,
fset-closed: (s closed under fs),
f-subset: xs ⊆ ys
FDL editor aliases :
fset-closure
Latex:
(c = fs closure of s) ==
s \msubseteq{} c \mwedge{} (c closed under fs) \mwedge{} (\mforall{}c':fset(T). (s \msubseteq{} c' {}\mRightarrow{} (c' closed under fs) {}\mRightarrow{} c \msubseteq{} c'))
Date html generated:
2016_05_14-PM-03_44_50
Last ObjectModification:
2015_10_06-PM-01_34_38
Theory : finite!sets
Home
Index