Function vstd::map_lib::lemma_map_new_values

source ·

pub proof fn lemma_map_new_values<K, V>(fk: FnSpec<(K,), bool>, fv: FnSpec<(K,), V>)

Expand description

ensures

Map::<K, V>::new(fk, fv).values()
    == Set::<V>::new(|v: V| (exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v)),

The set of values of a map constructed with Map::new(fk, fv) is equivalent to the set constructed with Set::new(|v: V| (exists |k: K| fk(k) && fv(k) == v). In other words, the set of all values fv(k) where fk(k) is true.