Skip to main content

lemma_injective_map_cardinality

vstd_extra::function_properties

Function lemma_injective_map_cardinality 

Source 
pub proof fn lemma_injective_map_cardinality<T, U>(
    f: FnSpec<(T,), U>,
    dom: Set<T>,
    s: Set<T>,
)
Expand description
requires
dom.injective_on(f),
s <= dom,
ensures
s.len() == s.map(f).len(),

Mapping a finite set with an injective function results in a set of the same cardinality.