Nuprl Definition : id-graph

Graph(S) ==  {i:Id| (i ∈ S)}  ⟶ ({i:Id| (i ∈ S)}  List)



Definitions occuring in Statement :  Id: Id l_member: (x ∈ l) list: List set: {x:A| B[x]}  function: x:A ⟶ B[x]
Definitions occuring in definition :  function: x:A ⟶ B[x] list: List set: {x:A| B[x]}  l_member: (x ∈ l) Id: Id
FDL editor aliases :  id-graph

Latex:
Graph(S)  ==    \{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  (\{i:Id|  (i  \mmember{}  S)\}    List)



Date html generated: 2016_05_14-PM-03_37_34
Last ObjectModification: 2015_09_22-PM-06_01_40

Theory : decidable!equality


Home Index