|
%--------------------------------------------------------------%
% Author: Dragan Stosic %
%--------------------------------------------------------------%
relation_inverse_extension[T, U: TYPE+]: THEORY
BEGIN
IMPORTING relation_inverse_image[T, U],
relation_inverse_image[U, T],
relation_extension[T, U]
f: VAR [T -> U]
g: VAR [U -> T]
m, n :VAR [T, U]
re_U: VAR equivalence[U]
re_T: VAR equivalence[T]
l_T(re_U, f):pred[[T, T]] = image_inverse(re_U, f)
le_U_induces_equivalence :JUDGEMENT l_T(re_U, f) HAS_TYPE equivalence[T]
l_U(re_T, g):pred[[U, U]] = image_inverse(re_T, g)
le_T_induces_equivalence: JUDGEMENT l_U(re_T, g) HAS_TYPE equivalence[U]
% etended equivalence relation based on inverse images of equivalence
% relations
rel_inv_extension(re_T, re_U, f, g) : set[[[T, U], [T, U]]] =
{ (m, n) | l_T(re_U, f)(n`1,m`1) AND l_U(re_T, g)(n`2,m`2) }
rel_inv_extension_is_equivalence: JUDGEMENT
rel_inv_extension(re_T, re_U, f, g) HAS_TYPE equivalence[[T, U]]
% connection between two relations:
% rel_extension and rel_image_extension
rel_extension_IFF_rel_ext : LEMMA
LET GFm=(g(m`2),f(m`1)), GFn=(g(n`2),f(n`1)) IN
rel_extension(re_T, re_U)(GFm, GFn) =
rel_inv_extension(re_T, re_U, f, g)(n, m)
% replaced: definition of the rel_inv_extension using the rel_extension
rel_inv_extension2(re_T, re_U, f, g):set[[[T, U], [T, U]]] =
{ (n, m) | LET GFm=(g(m`2),f(m`1)), GFn=(g(n`2),f(n`1)) IN
rel_extension(re_T, re_U)(GFm, GFn)
}
rel_inv_extension2_is_equivalence: JUDGEMENT
rel_inv_extension2(re_T, re_U, f, g) HAS_TYPE equivalence[[T, U]]
END relation_inverse_extension
¤ Dauer der Verarbeitung: 0.15 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.
|
