Nuprl Definition : K-le

i ≤ j == (fst(snd(fst(K)))) i j

Definitions occuring in Statement : pi1: fst(t), pi2: snd(t), apply: f a
Definitions occuring in definition : apply: f a, pi2: snd(t), pi1: fst(t)
FDL editor aliases : K-le

Latex:
i \mleq{} j == (fst(snd(fst(K)))) i j Date html generated: 2019_10_16-AM-11_44_08 Last ObjectModification: 2018_10_13-AM-11_56_16 Theory : minimal-first-order-logic Home Index