MapLemmas

📁 Source: Mathlib/Data/Vector/MapLemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems mapAccumr_bisim, mapAccumr_bisim_tail, mapAccumr_eq_map, mapAccumr_eq_map_of_constant_state, mapAccumr_eq_map_of_unused_state, mapAccumr_map, mapAccumr_mapAccumr, mapAccumr_mapAccumr₂, mapAccumr_redundant_pair, mapAccumr₂_bisim, mapAccumr₂_bisim_tail, mapAccumr₂_comm, mapAccumr₂_eq_map₂, mapAccumr₂_eq_map₂_of_constant_state, mapAccumr₂_eq_map₂_of_unused_state, mapAccumr₂_flip, mapAccumr₂_mapAccumr_left, mapAccumr₂_mapAccumr_right, mapAccumr₂_mapAccumr₂_left_left, mapAccumr₂_mapAccumr₂_left_right, mapAccumr₂_mapAccumr₂_right_left, mapAccumr₂_mapAccumr₂_right_right, mapAccumr₂_redundant_pair, mapAccumr₂_unused_input_left, mapAccumr₂_unused_input_right, map_eq_mapAccumr, map_map, map_mapAccumr, map_map₂, map_pmap, map₂_comm, map₂_eq_mapAccumr₂, map₂_flip, map₂_map_left, map₂_map_right, pmap_map	36
Total	36

List.Vector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapAccumr_bisim 📖	mathematical	—	List.Vector mapAccumr	—	mapAccumr_snoc
mapAccumr_bisim_tail 📖	mathematical	—	List.Vector mapAccumr	—	mapAccumr_bisim
mapAccumr_eq_map 📖	mathematical	Set Set.instMembership	List.Vector mapAccumr map	—	map_eq_mapAccumr mapAccumr_bisim_tail
mapAccumr_eq_map_of_constant_state 📖	mathematical	—	mapAccumr List.Vector map	—	mapAccumr_snoc map_snoc
mapAccumr_eq_map_of_unused_state 📖	mathematical	—	List.Vector mapAccumr map	—	mapAccumr_eq_map
mapAccumr_map 📖	mathematical	—	mapAccumr map	—	map_snoc mapAccumr_snoc
mapAccumr_mapAccumr 📖	mathematical	—	mapAccumr List.Vector	—	mapAccumr_snoc
mapAccumr_mapAccumr₂ 📖	mathematical	—	mapAccumr List.Vector mapAccumr₂	—	mapAccumr₂_snoc mapAccumr_snoc
mapAccumr_redundant_pair 📖	mathematical	—	List.Vector mapAccumr	—	mapAccumr_bisim_tail
mapAccumr₂_bisim 📖	mathematical	—	List.Vector mapAccumr₂	—	mapAccumr₂_snoc
mapAccumr₂_bisim_tail 📖	mathematical	—	List.Vector mapAccumr₂	—	mapAccumr₂_bisim
mapAccumr₂_comm 📖	mathematical	—	mapAccumr₂	—	—
mapAccumr₂_eq_map₂ 📖	mathematical	Set Set.instMembership	List.Vector mapAccumr₂ map₂	—	map₂_eq_mapAccumr₂ mapAccumr₂_bisim_tail
mapAccumr₂_eq_map₂_of_constant_state 📖	mathematical	—	mapAccumr₂ List.Vector map₂	—	mapAccumr₂_snoc map₂_snoc
mapAccumr₂_eq_map₂_of_unused_state 📖	mathematical	—	List.Vector mapAccumr₂ map₂	—	mapAccumr₂_eq_map₂
mapAccumr₂_flip 📖	mathematical	—	mapAccumr₂	—	—
mapAccumr₂_mapAccumr_left 📖	mathematical	—	mapAccumr₂ List.Vector mapAccumr	—	mapAccumr_snoc mapAccumr₂_snoc
mapAccumr₂_mapAccumr_right 📖	mathematical	—	mapAccumr₂ List.Vector mapAccumr	—	mapAccumr_snoc mapAccumr₂_snoc
mapAccumr₂_mapAccumr₂_left_left 📖	mathematical	—	mapAccumr₂ List.Vector	—	mapAccumr₂_snoc
mapAccumr₂_mapAccumr₂_left_right 📖	mathematical	—	mapAccumr₂ List.Vector	—	mapAccumr₂_snoc
mapAccumr₂_mapAccumr₂_right_left 📖	mathematical	—	mapAccumr₂ List.Vector	—	mapAccumr₂_snoc
mapAccumr₂_mapAccumr₂_right_right 📖	mathematical	—	mapAccumr₂ List.Vector	—	mapAccumr₂_snoc
mapAccumr₂_redundant_pair 📖	mathematical	—	List.Vector mapAccumr₂	—	mapAccumr₂_bisim_tail
mapAccumr₂_unused_input_left 📖	mathematical	—	mapAccumr₂ mapAccumr	—	mapAccumr₂_snoc mapAccumr_snoc
mapAccumr₂_unused_input_right 📖	mathematical	—	mapAccumr₂ mapAccumr	—	mapAccumr₂_snoc mapAccumr_snoc
map_eq_mapAccumr 📖	mathematical	—	map List.Vector mapAccumr	—	map_snoc mapAccumr_snoc
map_map 📖	mathematical	—	map	—	map_cons
map_mapAccumr 📖	mathematical	—	map List.Vector mapAccumr	—	mapAccumr_snoc map_snoc
map_map₂ 📖	mathematical	—	map map₂	—	map₂_snoc map_snoc
map_pmap 📖	mathematical	—	map pmap	—	toList_cons map_cons
map₂_comm 📖	mathematical	—	map₂	—	—
map₂_eq_mapAccumr₂ 📖	mathematical	—	map₂ List.Vector mapAccumr₂	—	map₂_snoc mapAccumr₂_snoc
map₂_flip 📖	mathematical	—	map₂	—	—
map₂_map_left 📖	mathematical	—	map₂ map	—	map_snoc map₂_snoc
map₂_map_right 📖	mathematical	—	map₂ map	—	map_snoc map₂_snoc
pmap_map 📖	mathematical	—	pmap map	—	map_cons toList_map toList_cons pmap.congr_simp

---

← Back to Index