|
%--------------------------------------------------------------%
% Author: Dragan Stosic %
%--------------------------------------------------------------%
relation_inverse_image[T, U: TYPE+]: THEORY
BEGIN
R: VAR pred[[U, U]]
f: VAR [T -> U]
t: VAR T
image_inverse(R, f):pred[[T, T]] = { (t1,t2:T) | R(f(t1),f(t2)) }
% The equivClass definition over the inverse image set
equivClass(R, f, t):pred[T] = { t1:T | image_inverse(R, f)(t, t1) }
% Curried form
image_inverse(R)(f):pred[[T, T]] = image_inverse(R, f)
% Curried form
equivClass(R, f)(t):pred[T] = equivClass(R, f, t)
equivClass_is_nonempty: LEMMA equivalence?[U](R)
IMPLIES nonempty?[T](equivClass(R,f)(t))
equivClass_equal_is_nonempty: LEMMA nonempty?[T](equivClass(=, f)(t))
inverse_image_of_equivalence: LEMMA equivalence?[U](R)
IMPLIES equivalence?[T](image_inverse(R, f))
preserves_eqv_of_inv_image: LEMMA EXISTS R: equivalence?[T](image_inverse(R, f))
inverse_image_of_equality: LEMMA equivalence?[T](image_inverse(=, f))
image_inverse_eq_is_eq_kernel: LEMMA
EquivalenceKernel[T, T, U](f) = image_inverse(=)(f)
inv_img_surj_impl_codom_eq: LEMMA
FORALL (f:(surjective?[T, U])):
equivalence?[T](image_inverse(R,f)) IMPLIES equivalence?[U](R)
right_inv_inv_finv_image_impl_codom_eq: LEMMA
right_inverse?(inverse(f), f) IMPLIES
equivalence?[T](image_inverse(R, f)) IMPLIES equivalence?[U](R)
surjective_eqv_image_inv_rel_codomain: THEOREM
FORALL (f:(surjective?[T, U])):
equivalence?[T](image_inverse(R)(f)) = equivalence?[U](R)
right_inv_inv_finv_image_eq_codom_eq: LEMMA
right_inverse?(inverse(f), f) IMPLIES
equivalence?[T](image_inverse(R, f)) = equivalence?[U](R)
END relation_inverse_image
¤ Dauer der Verarbeitung: 0.16 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.
|
