Lemmas

Statistics

Metric	Count
Definitions	0
Theorems `foldl_range_eq_of_range_eq`, `foldl_range_subset_of_range_subset`, `foldr_range_eq_of_range_eq`, `foldr_range_subset_of_range_subset`, `injOn_insertIdx_index_of_notMem`, `mapAccumr_eq_foldr`, `mapAccumr₂_eq_foldr`, `setOf_mem_eq_empty_iff`	8
Total	8

Name	Kind	Assumes	Proves	Validates	Depends On
`foldl_range_eq_of_range_eq` 📖	—	`Set.range`	—	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `foldl_range_subset_of_range_subset` `Eq.le` `Eq.ge`
`foldl_range_subset_of_range_subset` 📖	—	`Set` `Set.instHasSubset` `Set.range`	—	—	`Set.range_comp'` `Function.Surjective.range_eq` `Function.Bijective.surjective` `Function.Involutive.bijective` `reverse_involutive` `Set.image_univ` `foldr_range_subset_of_range_subset`
`foldr_range_eq_of_range_eq` 📖	—	`Set.range`	—	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `foldr_range_subset_of_range_subset` `Eq.le` `Eq.ge`
`foldr_range_subset_of_range_subset` 📖	—	`Set` `Set.instHasSubset` `Set.range`	—	—	`Set.mem_range_self`
`injOn_insertIdx_index_of_notMem` 📖	mathematical	—	`Set.InjOn` `setOf`	—	—
`mapAccumr_eq_foldr` 📖	mathematical	—	`mapAccumr`	—	—
`mapAccumr₂_eq_foldr` 📖	mathematical	—	`mapAccumr₂`	—	—
`setOf_mem_eq_empty_iff` 📖	mathematical	—	`setOf` `Set` `Set.instEmptyCollection`	—	`Set.eq_empty_iff_forall_notMem`

---