Nuprl Definition : lattice-bless
lattice-bless(l;eq;a;b) == lattice-ble(l;eq;a;b) ∧b (¬b(eq a b))
Definitions occuring in Statement :
lattice-ble: lattice-ble(l;eq;a;b),
band: p ∧b q,
bnot: ¬bb,
apply: f a
Definitions occuring in definition :
band: p ∧b q,
lattice-ble: lattice-ble(l;eq;a;b),
bnot: ¬bb,
apply: f a
FDL editor aliases :
lattice-bless
Latex:
lattice-bless(l;eq;a;b) == lattice-ble(l;eq;a;b) \mwedge{}\msubb{} (\mneg{}\msubb{}(eq a b))
Date html generated:
2016_05_18-AM-11_23_34
Last ObjectModification:
2015_10_06-PM-01_44_40
Theory : lattices
Home
Index