Nuprl Definition : irrefl

(basic):: Irrefl(T;x,y.E[x; y]) ==  ∀[a:T]. (¬E[a; a])


Definitions occuring in Statement :  uall: ∀[x:A]. B[x],  not: ¬A
Definitions occuring in definition :  uall: ∀[x:A]. B[x],  not: ¬A
FDL editor aliases :  irrefl
Latex:
(basic)::  Irrefl(T;x,y.E[x;  y])  ==    \mforall{}[a:T].  (\mneg{}E[a;  a])


Date html generated: 2016_05_13-PM-04_17_24
Last ObjectModification: 2015_09_22-PM-05_46_11

Theory : rel_1


Home Index