Nuprl Definition : fset_mem
x ↓∈ s == ↓∃L:T List. ((L = s ∈ fset(T)) ∧ (x ∈ L))
Definitions occuring in Statement :
fset: fset(T),
l_member: (x ∈ l),
list: T List,
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
squash: ↓T,
exists: ∃x:A. B[x],
list: T List,
and: P ∧ Q,
equal: s = t ∈ T,
fset: fset(T),
l_member: (x ∈ l)
FDL editor aliases :
fset_mem
Latex:
x \mdownarrow{}\mmember{} s == \mdownarrow{}\mexists{}L:T List. ((L = s) \mwedge{} (x \mmember{} L))
Date html generated:
2016_05_14-PM-03_38_02
Last ObjectModification:
2015_10_06-PM-01_37_48
Theory : finite!sets
Home
Index