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
injective_on(f, dom),
s.finite(),
s <= dom,
ensures
s.len() == s.map(f).len(),
s.map(f).finite(),

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