|
%--------------------------------------------------------------%
% Author: Dragan Stosic %
%--------------------------------------------------------------%
relational_choice_properties[T, U: TYPE+]: THEORY
BEGIN
IMPORTING relational_choice[T, U]
fun_choice_impl_description: LEMMA fun_choice IMPLIES parametric_definite_description
fun_choice_impl_rel_unique_choice: LEMMA fun_choice IMPLIES rel_unique_choice
fun_choice_impl_rel_choice: LEMMA fun_choice IMPLIES rel_choice
fun_choice_impl_rel_choice_impl_description_rel_choice: LEMMA
fun_choice IMPLIES rel_choice IMPLIES parametric_definite_description
fun_choice_impl_rel_choice_and_description_rel_choice: LEMMA
fun_choice IMPLIES rel_choice AND parametric_definite_description
fun_choice_impl_rel_unique_choice_impl_description_rel_choice: LEMMA
fun_choice IMPLIES rel_unique_choice IMPLIES parametric_definite_description
fun_choice_impl_rel_unique_choice_and_description_rel_choice: LEMMA
fun_choice IMPLIES rel_unique_choice AND parametric_definite_description
description_rel_unique_choice_imp_funct_choice: LEMMA
parametric_definite_description IMPLIES rel_unique_choice IMPLIES fun_choice
description_rel_and_rel_unique_choice_imp_funct_choice: LEMMA
parametric_definite_description AND rel_unique_choice IMPLIES fun_choice
rel_choice_and_proof_irrel_imp_guarded_rel_choice: LEMMA
rel_unique_choice IMPLIES proof_irrelevance IMPLIES conditional_relational_choice
relx_choice_indep_of_premises_imp_guarded_rel_choice: LEMMA
rel_unique_choice IMPLIES independence_of_premises IMPLIES conditional_relational_choice
fun_choice_equiv_rel_unique_param_desc: THEOREM
fun_choice IFF rel_unique_choice AND parametric_definite_description
END relational_choice_properties
¤ Dauer der Verarbeitung: 0.1 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.
|
