Nuprl Definition : isdM1
isdM1(x) == deq-fset(deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq))) x {{}}
Definitions occuring in Statement :
names-deq: NamesDeq,
names: names(I),
deq-fset: deq-fset(eq),
empty-fset: {},
fset-singleton: {x},
union-deq: union-deq(A;B;a;b),
apply: f a
Definitions occuring in definition :
apply: f a,
deq-fset: deq-fset(eq),
union-deq: union-deq(A;B;a;b),
names: names(I),
names-deq: NamesDeq,
fset-singleton: {x},
empty-fset: {}
FDL editor aliases :
isdM1
Latex:
isdM1(x) == deq-fset(deq-fset(union-deq(names(I);names(I);NamesDeq;NamesDeq))) x \{\{\}\}
Date html generated:
2016_05_18-AM-11_56_54
Last ObjectModification:
2016_02_04-PM-06_14_42
Theory : cubical!type!theory
Home
Index