Nuprl Definition : lattice-extend

lattice-extend(L;eq;eqL;f;ac) ==  \/(λxs./\(f"(xs))"(ac))



Definitions occuring in Statement :  lattice-fset-join: \/(s) lattice-fset-meet: /\(s) fset-image: f"(s) deq-fset: deq-fset(eq) lambda: λx.A[x]
Definitions occuring in definition :  lattice-fset-join: \/(s) deq-fset: deq-fset(eq) lambda: λx.A[x] lattice-fset-meet: /\(s) fset-image: f"(s)
FDL editor aliases :  lattice-extend

Latex:
lattice-extend(L;eq;eqL;f;ac)  ==    \mbackslash{}/(\mlambda{}xs./\mbackslash{}(f"(xs))"(ac))



Date html generated: 2020_05_20-AM-08_45_29
Last ObjectModification: 2015_10_06-PM-01_43_45

Theory : lattices


Home Index