Module set_extra

Module set_extra 

Source
Expand description

Extra properties of vstd::set::Set.

Functionsยง

is_partition
lemma_empty_bad_set_implies_forall
lemma_filter_all_false
lemma_filter_len_unchanged_implies_equal
lemma_flatten_cardinality_under_disjointness
lemma_flatten_cardinality_under_disjointness_same_length
lemma_full_good_set_implies_forall
lemma_insert_filter_false
lemma_insert_filter_true
lemma_nat_range_finite
lemma_remove_filter_true
lemma_set_prop_mutual_exclusion
lemma_set_separation
pairwise_disjoint
set_prop_mutual_exclusion