Spracherkennung für: .dep vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
/top,fun_below_props,power_sets,set_of_functions,bits,card_comp,card_comp_props,card_comp_set,card_comp_set_props,card_comp_set_transitive,card_comp_transitive,card_finite,card_power,card_power_set,card_sets_lemmas,card_single,card_function,cardinal,countability,countable_image,infinite_image,countable_props,infinite_nat_def,countable_set,countable_setofsets,countable_types,infinite_card,infinite_sets,sets_lemmas_extra,indexed_sets_aux,countable_indexed_sets,nat_indexed_sets,inverse_image_Union,countability_aux,cantor_bernstein_schroeder,top_choice_facts,relational_choice,relation_implication,relational_choice_properties,top_refinement_relations,relation_extension,relation_extension_props,relation_inverse_image,relation_inverse_extension,rr_rel,simplest_examples,singleton_example,finite_nats_trivial,infinite_to_infinite_trivial,finite_to_infinite,infinite_to_finite_finite_equival_finite_equival_classes,infinite_to_finite_infinite_equival_finite_equival_classes,infinite_to_infinite_infinite_equival_infinite_equival_classes,infinite_to_infinite_infinite_equival_finite_equival_classes,finite_to_infinite_finite_equival_infinite_equival_classes
structures/fun_preds_partial
orders/relations_extra,lattices,bounded_orders,minmax_orders,numbers_infinite,bounded_integers,chain_chain,ordered_subset,set_antisymmetric,relation_iterate,integer_enumerations,zorn,total_lattices,non_empty_bounded_sets,upper_semilattices,bounded_sets,chain,indexed_sets_extra,set_dichotomous,lower_semilattices,bounded_nats,subset_chain,closure_ops
finite_sets/func_composition,finite_sets_minmax,finite_sets_eq,finite_sets_inductions,finite_sets_card_eq
ints/div,floor_div_lems,abs_rews
top:fun_below_props,power_sets,set_of_functions,bits,card_comp,card_comp_props,card_comp_set,card_comp_set_props,card_comp_set_transitive,card_comp_transitive,card_finite,card_power,card_power_set,card_sets_lemmas,card_single,cardinal,countability,countable_props,countable_set,countable_setofsets,countable_types,infinite_card,infinite_image,infinite_sets,sets_lemmas_extra,countable_image,card_function,infinite_nat_def,indexed_sets_aux,countable_indexed_sets,nat_indexed_sets,inverse_image_Union,countability_aux,cantor_bernstein_schroeder,top_choice_facts,top_refinement_relations
fun_below_props:
power_sets:finite_sets@finite_sets_card_eq,set_of_functions,finite_sets@finite_sets_eq
set_of_functions:fun_below_props,finite_sets@func_composition
bits:orders@bounded_nats
card_comp:
card_comp_props:card_comp,orders@set_dichotomous,orders@set_antisymmetric
card_comp_set:
card_comp_set_props:card_comp_set,orders@set_dichotomous,orders@set_antisymmetric
card_comp_set_transitive:card_comp_set,orders@set_dichotomous
card_comp_transitive:card_comp,orders@set_dichotomous
card_finite:card_comp_set_props
card_power:card_comp_props
card_power_set:card_comp_set_props
card_sets_lemmas:card_single
card_single:card_comp_set_props,card_comp_set_transitive
card_function:
cardinal:card_finite,card_single
countability:orders@integer_enumerations
countable_image:countability,infinite_image,card_function
infinite_image:
countable_props:countability,infinite_nat_def,card_comp_set_props
infinite_nat_def:
countable_set:bits,orders@set_antisymmetric
countable_setofsets:countable_set,countable_props
countable_types:countability,countable_set,countable_props,infinite_nat_def,orders@numbers_infinite
infinite_card:card_comp_set_props
infinite_sets:countable_props,card_sets_lemmas
sets_lemmas_extra:
indexed_sets_aux:
countable_indexed_sets:indexed_sets_aux,countability
nat_indexed_sets:structures@fun_preds_partial,indexed_sets_aux
inverse_image_Union:
countability_aux:countability,countable_props
cantor_bernstein_schroeder:
top_choice_facts:relational_choice,relational_choice_properties,relation_implication
relational_choice:relation_implication
relation_implication:
relational_choice_properties:relational_choice
top_refinement_relations:relation_extension,relation_extension_props,relation_inverse_image,relation_inverse_extension,rr_rel,simplest_examples
relation_extension:
relation_extension_props:relation_extension
relation_inverse_image:
relation_inverse_extension:relation_inverse_image,relation_extension
rr_rel:relation_extension,relation_inverse_extension
simplest_examples:singleton_example,finite_nats_trivial,infinite_to_infinite_trivial,finite_to_infinite,infinite_to_finite_finite_equival_finite_equival_classes,infinite_to_finite_infinite_equival_finite_equival_classes,infinite_to_infinite_infinite_equival_infinite_equival_classes,infinite_to_infinite_infinite_equival_finite_equival_classes,finite_to_infinite_finite_equival_infinite_equival_classes
singleton_example:rr_rel
finite_nats_trivial:ints@div,rr_rel
infinite_to_infinite_trivial:ints@div,rr_rel
finite_to_infinite:rr_rel
infinite_to_finite_finite_equival_finite_equival_classes:rr_rel
infinite_to_finite_infinite_equival_finite_equival_classes:rr_rel
infinite_to_infinite_infinite_equival_infinite_equival_classes:rr_rel
infinite_to_infinite_infinite_equival_finite_equival_classes:ints@div,rr_rel
finite_to_infinite_finite_equival_infinite_equival_classes:rr_rel
