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