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_46
Last ObjectModification:
2015_10_06-PM-01_43_34
Theory : lattices
Home
Index