|
%--------------------------------------------------------------%
% Author: Dragan Stosic %
%--------------------------------------------------------------%
relation_extension_props[T, U: TYPE+]: THEORY
BEGIN
IMPORTING relation_extension
le_T: VAR equivalence[T]
le_U: VAR equivalence[U]
m, n: VAR [T, U]
% NON-EMPTY LEMMAS
extended_equiv_class_non_empty: LEMMA
nonempty?[[T,U]](extended_equiv_class(rel_extension(le_T, le_U))(m))
nonempty_equivClass_impl_extended_equiv_class_non_empty: LEMMA
nonempty?[T](EquivClass(le_T)(m`1)) IFF
nonempty?[[T,U]](extended_equiv_class(rel_extension(le_T, le_U))(m))
nonempty_equivClass_iff_extended_equiv_classT_non_empty: LEMMA
nonempty?[T](EquivClass(le_T)(m`1)) IFF
nonempty?[T](extended_equiv_classT(
rel_extension(le_T, le_U),proj_tuple_1, m, m))
nonempty_equivClass_iff_extended_equiv_classU_non_empty: LEMMA
nonempty?[T](EquivClass(le_T)(m`1)) IFF
nonempty?[U](extended_equiv_classU(
rel_extension(le_T, le_U),proj_tuple_2, m, m))
% CLASS REPRESENTATIVE LEMMAS
proj_tuple_1_equiv_class_representative: LEMMA
m`1 = repEC_ext(le_T, le_U, m)`1 IMPLIES
le_T( proj_tuple_1(repEC_ext(le_T, le_U, m)), repEC(le_T)(m`1))
proj_tuple_2_equiv_class_representative: LEMMA
m`2 = repEC_ext(le_T, le_U, m)`2 IMPLIES
le_U( proj_tuple_2(repEC_ext(le_T, le_U, m)), repEC(le_U)(m`2));
END relation_extension_props
¤ Dauer der Verarbeitung: 0.21 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.
|
