Module function_properties

Module function_properties 

Source
Expand description

Properties of pure mathematical spec functions (spec_fn).

Functionsยง

bijective_on
construct_inverse
construct_left_inverse
inverse_on
left_inverse_on
lemma_bijective_cardinality
lemma_bijective_subset_still_bijective
lemma_construct_inverse_sound
lemma_construct_left_inverse_sound
lemma_injective_implies_injective_on
lemma_injective_map_cardinality
lemma_inverse_of_bijection_is_bijective
lemma_left_inverse_of_bijection_is_bijective
lemma_right_inverse_of_bijection_is_bijective
lemma_two_sided_inverse_implies_bijective
right_inverse_on