Nuprl Definition : id-fun

id-fun(T) ==  x:T ⟶ {y:T| x = y ∈ T} 


Definitions occuring in Statement :  set: {x:A| B[x]} ,  function: x:A ⟶ B[x],  equal: s = t ∈ T
Definitions occuring in definition :  function: x:A ⟶ B[x],  set: {x:A| B[x]} ,  equal: s = t ∈ T
FDL editor aliases :  id-fun
Latex:
id-fun(T)  ==    x:T  {}\mrightarrow{}  \{y:T|  x  =  y\} 


Date html generated: 2016_05_13-PM-03_46_06
Last ObjectModification: 2015_09_22-PM-05_45_12

Theory : call!by!value_2


Home Index