|
% Ordered sets (T, <=) that have a "complement" function, i.e.,
% an involutorian, anti-monotone function from T to T.
%
complementary_orders[T: TYPE+]: THEORY
BEGIN
IMPORTING bounded_orders[T]
rel: VAR pred[[T, T]]
C: VAR [T -> T]
t, t1, t2: VAR T
S: VAR set[T]
complement?(rel)(C): bool =
C o C = id[T] & preserves(C, rel, converse(rel))
% complement_is_bijective: JUDGEMENT
% (complement?(rel)) SUBTYPE_OF (bijective?[T, T])
complement_complement: LEMMA
FORALL (C: (complement?(rel))): C(C(t)) = t
image_complement: LEMMA
FORALL (C: (complement?(rel))): image(C, image(C, S)) = S
inverse_complement: LEMMA
FORALL (C: (complement?(rel))): inverse[T, T](C) = C
% inverse_complement_is_complement: JUDGEMENT
% inverse[T, T](C: (complement?(rel))) HAS_TYPE (complement?(rel))
le_complement: LEMMA
FORALL (C: (complement?(rel))): rel(C(t1), C(t2)) IFF rel(t2, t1)
upper_bound_complement: LEMMA
FORALL (C: (complement?(rel))):
upper_bound?[T](t, S, rel) IFF lower_bound?[T](C(t), image(C, S), rel)
bounded_above_complement: LEMMA
FORALL (C: (complement?(rel))):
bounded_above?[T](S, rel) IFF bounded_below?[T](image(C, S), rel)
least_upper_bound_complement: LEMMA
FORALL (C: (complement?(rel))):
least_upper_bound?[T](t, S, rel) IFF
greatest_lower_bound?[T](C(t), image(C, S), rel)
least_bounded_above_complement: LEMMA
FORALL (C: (complement?(rel))):
least_bounded_above?[T](S, rel) IFF
greatest_bounded_below?[T](image(C, S), rel)
lub_complement: LEMMA
FORALL (rel: (antisymmetric?[T]), C: (complement?(rel)),
S: (least_bounded_above?(rel))):
lub[T](rel)(S) = C(glb[T](rel)(image(C, S)))
glb_complement: LEMMA
FORALL (rel: (antisymmetric?[T]), C: (complement?(rel)),
S: (greatest_bounded_below?(rel))):
glb[T](rel)(S) = C(lub[T](rel)(image(C, S)))
END complementary_orders
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
