Nuprl Definition : opposite-lattice
opposite-lattice(L) == {points=Point(L);meet=λ2a b.a ∨ b;join=λ2a b.a ∧ b;0=1;1=0}
Definitions occuring in Statement :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
lattice-0: 0,
lattice-1: 1,
lattice-join: a ∨ b,
lattice-meet: a ∧ b,
lattice-point: Point(l),
so_lambda: λ2x y.t[x; y]
Definitions occuring in definition :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
lattice-point: Point(l),
lattice-join: a ∨ b,
so_lambda: λ2x y.t[x; y],
lattice-meet: a ∧ b,
lattice-1: 1,
lattice-0: 0
FDL editor aliases :
opposite-lattice
Latex:
opposite-lattice(L) == \{points=Point(L);meet=\mlambda{}\msubtwo{}a b.a \mvee{} b;join=\mlambda{}\msubtwo{}a b.a \mwedge{} b;0=1;1=0\}
Date html generated:
2020_05_20-AM-08_47_01
Last ObjectModification:
2015_10_08-PM-11_00_35
Theory : lattices
Home
Index