|
% Lattices that have a "complement" function. See also complementary_orders.
%
complementary_lattices[
T: TYPE+,
(IMPORTING bounded_orders[T])
<=: (lattice?[T])
]: THEORY
BEGIN
IMPORTING
lattices[T, <=],
minmax_orders[T],
function_image_extra[T, T],
complementary_orders[T]
t, t1, t2: VAR T
C, H: VAR [T -> T]
S: VAR set[T]
NF: VAR non_empty_finite_set[T]
% modular?(<=): bool =
% FORALL (a, c: T):
% a <= c => lub(<=)(a, glb(<=)(b, c)) = glb(<=)(lub(<=)(a, b), c)
dual(C)(H): [T -> T] = C o H o C
dual_dual : LEMMA
FORALL (C: (complement?(<=))): dual(C)(dual(C)(H)) = H
dual_inclusion1 : LEMMA
FORALL (C: (complement?(<=))): H(C(t)) <= C(t) IFF t <= dual(C)(H)(t)
dual_inclusion2 : LEMMA
FORALL (C: (complement?(<=))): C(t) <= H(C(t)) IFF dual(C)(H)(t) <= t
dual_inclusion3 : LEMMA
FORALL (C: (complement?(<=))): H(t) <= t IFF C(t) <= dual(C)(H)(C(t))
dual_inclusion4 : LEMMA
FORALL (C: (complement?(<=))): t <= H(t) IFF dual(C)(H)(C(t)) <= C(t)
END complementary_lattices
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
