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