AList

📁 Source: Mathlib/Data/List/AList.lean

Statistics

Metric	Count
Definitions `AList`, `entries`, `erase`, `extract`, `foldl`, `insert`, `insertRec`, `instDecidableEq`, `instDecidableMem`, `instEmptyCollection`, `instInhabited`, `instMembership`, `instUnion`, `keys`, `lookup`, `replace`, `singleton`, `union`, `toAList`	19
Theorems `empty_entries`, `empty_union`, `entries_insert`, `entries_insert_of_notMem`, `entries_toAList`, `erase_erase`, `ext`, `ext_iff`, `extract_eq_lookup_erase`, `insertRec_empty`, `insertRec_insert`, `insertRec_insert_mk`, `insert_empty`, `insert_insert`, `insert_insert_of_ne`, `insert_of_notMem`, `insert_singleton_eq`, `insert_union`, `keys_empty`, `keys_erase`, `keys_insert`, `keys_mk`, `keys_nodup`, `keys_replace`, `keys_singleton`, `keys_subset_keys_of_entries_subset_entries`, `lookup_empty`, `lookup_eq_none`, `lookup_erase`, `lookup_erase_ne`, `lookup_insert`, `lookup_insert_eq_none`, `lookup_insert_ne`, `lookup_isSome`, `lookup_to_alist`, `lookup_union_eq_some`, `lookup_union_left`, `lookup_union_right`, `mem_erase`, `mem_insert`, `mem_keys`, `mem_lookup_iff`, `mem_lookup_union`, `mem_lookup_union_middle`, `mem_mk`, `mem_of_perm`, `mem_replace`, `mem_union`, `mk_cons_eq_insert`, `nodupKeys`, `notMem_empty`, `perm_erase`, `perm_insert`, `perm_lookup`, `perm_replace`, `perm_union`, `singleton_entries`, `toAList_cons`, `union_assoc`, `union_comm_of_disjoint`, `union_empty`, `union_entries`, `union_erase`	63
Total	82

AList

Definitions

Name	Category	Theorems
`entries` 📖	CompOp	17 math math: `toFinmap_entries`, `toFinmap_eq`, `ext_iff`, `entries_insert`, `empty_entries`, `singleton_entries`, `lookupFinsupp_support`, `union_comm_of_disjoint`, `Finsupp.toAList_entries`, `union_assoc`, `entries_toAList`, `entries_insert_of_notMem`, `insert_of_notMem`, `insert_insert_of_ne`, `union_entries`, `mem_lookup_iff`, `nodupKeys`
`erase` 📖	CompOp	10 math math: `erase_erase`, `mem_erase`, `union_erase`, `lookup_erase_ne`, `perm_erase`, `keys_erase`, `extract_eq_lookup_erase`, `Finmap.keys_erase_toFinset`, `Finmap.erase_toFinmap`, `lookup_erase`
`extract` 📖	CompOp	1 math math: `extract_eq_lookup_erase`
`foldl` 📖	CompOp	—
`insert` 📖	CompOp	20 math math: `insert_empty`, `perm_insert`, `keys_insert`, `lookup_insert_ne`, `insertRec_insert`, `lookup_insert`, `entries_insert`, `insert_singleton_eq`, `insert_insert`, `toAList_cons`, `mem_insert`, `Finmap.insert_toFinmap`, `insert_union`, `entries_insert_of_notMem`, `insert_of_notMem`, `mk_cons_eq_insert`, `insert_insert_of_ne`, `insertRec_insert_mk`, `lookup_insert_eq_none`, `insert_lookupFinsupp`
`insertRec` 📖	CompOp	3 math math: `insertRec_insert`, `insertRec_empty`, `insertRec_insert_mk`
`instDecidableEq` 📖	CompOp	—
`instDecidableMem` 📖	CompOp	—
`instEmptyCollection` 📖	CompOp	10 math math: `notMem_empty`, `insert_empty`, `empty_lookupFinsupp`, `empty_union`, `empty_entries`, `insertRec_empty`, `Finmap.empty_toFinmap`, `lookup_empty`, `keys_empty`, `union_empty`
`instInhabited` 📖	CompOp	—
`instMembership` 📖	CompOp	15 math math: `mem_erase`, `notMem_empty`, `lookupFinsupp_eq_zero_iff`, `mem_keys`, `mem_union`, `mem_of_perm`, `mem_replace`, `mem_insert`, `mem_lookup_union`, `Finsupp.mem_toAlist`, `mem_mk`, `lookup_isSome`, `lookup_union_eq_some`, `lookup_eq_none`, `Finmap.mem_toFinmap`
`instUnion` 📖	CompOp	14 math math: `union_erase`, `empty_union`, `lookup_union_left`, `mem_union`, `perm_union`, `union_comm_of_disjoint`, `mem_lookup_union`, `insert_union`, `union_assoc`, `Finmap.union_toFinmap`, `union_entries`, `lookup_union_eq_some`, `lookup_union_right`, `union_empty`
`keys` 📖	CompOp	12 math math: `keys_nodup`, `keys_insert`, `mem_keys`, `keys_subset_keys_of_entries_subset_entries`, `Finmap.keys_ext`, `keys_replace`, `keys_singleton`, `keys_erase`, `Finmap.keys_val`, `keys_empty`, `keys_mk`, `Finsupp.toAList_keys_toFinset`
`lookup` 📖	CompOp	20 math math: `lookupFinsupp_eq_zero_iff`, `lookup_insert_ne`, `lookup_erase_ne`, `lookupFinsupp_eq_iff_of_ne_zero`, `lookup_insert`, `lookup_union_left`, `lookup_to_alist`, `mem_lookup_union`, `extract_eq_lookup_erase`, `lookup_empty`, `lookup_isSome`, `lookup_erase`, `lookupFinsupp_apply`, `Finmap.lookup_toFinmap`, `lookup_insert_eq_none`, `lookup_union_eq_some`, `mem_lookup_iff`, `lookup_union_right`, `lookup_eq_none`, `perm_lookup`
`replace` 📖	CompOp	4 math math: `perm_replace`, `keys_replace`, `mem_replace`, `Finmap.replace_toFinmap`
`singleton` 📖	CompOp	5 math math: `insert_empty`, `keys_singleton`, `singleton_entries`, `insert_singleton_eq`, `singleton_lookupFinsupp`
`union` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty_entries` 📖	mathematical	—	`entries` `AList` `instEmptyCollection`	—	—
`empty_union` 📖	mathematical	—	`AList` `instUnion` `instEmptyCollection`	—	`ext`
`entries_insert` 📖	mathematical	—	`entries` `insert` `List.kerase`	—	—
`entries_insert_of_notMem` 📖	mathematical	`AList` `instMembership`	`entries` `insert`	—	`entries_insert` `List.kerase_of_notMem_keys`
`entries_toAList` 📖	mathematical	—	`entries` `List.toAList` `List.dedupKeys`	—	—
`erase_erase` 📖	mathematical	—	`erase`	—	`ext` `List.kerase_kerase`
`ext` 📖	—	`entries`	—	—	—
`ext_iff` 📖	mathematical	—	`entries`	—	`ext`
`extract_eq_lookup_erase` 📖	mathematical	—	`extract` `AList` `lookup` `erase`	—	`List.kextract_eq_dlookup_kerase`
`insertRec_empty` 📖	mathematical	—	`insertRec` `AList` `instEmptyCollection`	—	`List.nodupKeys_nil` `insertRec.eq_1`
`insertRec_insert` 📖	mathematical	`AList` `instMembership`	`insertRec` `insert`	—	`List.nodupKeys_cons` `List.nodupKeys_of_nodupKeys_cons` `insertRec.eq_2` `nodupKeys` `insert_of_notMem`
`insertRec_insert_mk` 📖	mathematical	`AList` `instMembership`	`insertRec` `insert`	—	`insertRec_insert`
`insert_empty` 📖	mathematical	—	`insert` `AList` `instEmptyCollection` `singleton`	—	—
`insert_insert` 📖	mathematical	—	`insert`	—	`ext` `List.kerase_cons_eq`
`insert_insert_of_ne` 📖	mathematical	—	`entries` `insert`	—	`List.kerase_cons_ne` `List.kerase_comm`
`insert_of_notMem` 📖	mathematical	`AList` `instMembership`	`insert` `entries` `List.NodupKeys` `List.keys` `List.nodupKeys_cons` `nodupKeys`	—	`ext` `List.nodupKeys_cons` `nodupKeys` `entries_insert_of_notMem`
`insert_singleton_eq` 📖	mathematical	—	`insert` `singleton`	—	`ext` `List.kerase_cons_eq`
`insert_union` 📖	mathematical	—	`insert` `AList` `instUnion`	—	`ext` `List.kunion_kerase`
`keys_empty` 📖	mathematical	—	`keys` `AList` `instEmptyCollection`	—	—
`keys_erase` 📖	mathematical	—	`keys` `erase`	—	`List.keys_kerase`
`keys_insert` 📖	mathematical	—	`keys` `insert`	—	`List.keys_kerase`
`keys_mk` 📖	mathematical	`List.NodupKeys`	`keys` `List.keys`	—	—
`keys_nodup` 📖	mathematical	—	`keys`	—	`nodupKeys`
`keys_replace` 📖	mathematical	—	`keys` `replace`	—	`List.keys_kreplace`
`keys_singleton` 📖	mathematical	—	`keys` `singleton`	—	—
`keys_subset_keys_of_entries_subset_entries` 📖	mathematical	`entries`	`keys`	—	`lookup_isSome` `mem_lookup_iff` `mem_keys`
`lookup_empty` 📖	mathematical	—	`lookup` `AList` `instEmptyCollection`	—	—
`lookup_eq_none` 📖	mathematical	—	`lookup` `AList` `instMembership`	—	`List.dlookup_eq_none`
`lookup_erase` 📖	mathematical	—	`lookup` `erase`	—	`List.dlookup_kerase` `nodupKeys`
`lookup_erase_ne` 📖	mathematical	—	`lookup` `erase`	—	`List.dlookup_kerase_ne`
`lookup_insert` 📖	mathematical	—	`lookup` `insert`	—	`List.dlookup_kinsert`
`lookup_insert_eq_none` 📖	mathematical	—	`lookup` `insert`	—	`lookup_insert` `lookup_insert_ne`
`lookup_insert_ne` 📖	mathematical	—	`lookup` `insert`	—	`List.dlookup_kinsert_ne`
`lookup_isSome` 📖	mathematical	—	`lookup` `AList` `instMembership`	—	`List.dlookup_isSome`
`lookup_to_alist` 📖	mathematical	—	`lookup` `List.toAList` `List.dlookup`	—	`List.nodupKeys_dedupKeys` `List.toAList.eq_1` `lookup.eq_1` `List.dlookup_dedupKeys`
`lookup_union_eq_some` 📖	mathematical	—	`lookup` `AList` `instUnion` `instMembership`	—	`List.mem_dlookup_kunion`
`lookup_union_left` 📖	mathematical	`AList` `instMembership`	`lookup` `instUnion`	—	`List.dlookup_kunion_left`
`lookup_union_right` 📖	mathematical	`AList` `instMembership`	`lookup` `instUnion`	—	`List.dlookup_kunion_right`
`mem_erase` 📖	mathematical	—	`AList` `instMembership` `erase`	—	`mem_keys` `keys_erase` `keys_nodup`
`mem_insert` 📖	mathematical	—	`AList` `instMembership` `insert`	—	`List.mem_keys_kinsert`
`mem_keys` 📖	mathematical	—	`AList` `instMembership` `keys`	—	—
`mem_lookup_iff` 📖	mathematical	—	`lookup` `entries`	—	`List.mem_dlookup_iff` `nodupKeys`
`mem_lookup_union` 📖	mathematical	—	`lookup` `AList` `instUnion` `instMembership`	—	`List.mem_dlookup_kunion`
`mem_lookup_union_middle` 📖	—	`lookup` `AList` `instUnion` `instMembership`	—	—	`List.mem_dlookup_kunion_middle`
`mem_mk` 📖	mathematical	`List.NodupKeys`	`AList` `instMembership` `List.keys`	—	—
`mem_of_perm` 📖	mathematical	`entries`	`AList` `instMembership`	—	—
`mem_replace` 📖	mathematical	—	`AList` `instMembership` `replace`	—	`mem_keys` `keys_replace`
`mem_union` 📖	mathematical	—	`AList` `instMembership` `instUnion`	—	`List.mem_keys_kunion`
`mk_cons_eq_insert` 📖	mathematical	`List.NodupKeys`	`insert` `List.nodupKeys_of_nodupKeys_cons`	—	`List.nodupKeys_of_nodupKeys_cons` `Sigma.eta` `List.kerase_of_notMem_keys` `List.notMem_keys_of_nodupKeys_cons`
`nodupKeys` 📖	mathematical	—	`List.NodupKeys` `entries`	—	—
`notMem_empty` 📖	mathematical	—	`AList` `instMembership` `instEmptyCollection`	—	—
`perm_erase` 📖	mathematical	`entries`	`erase`	—	`List.Perm.kerase` `nodupKeys`
`perm_insert` 📖	mathematical	`entries`	`insert`	—	`List.Perm.kinsert` `nodupKeys`
`perm_lookup` 📖	mathematical	`entries`	`lookup`	—	`List.perm_dlookup` `nodupKeys`
`perm_replace` 📖	mathematical	`entries`	`replace`	—	`List.Perm.kreplace` `nodupKeys`
`perm_union` 📖	mathematical	`entries`	`AList` `instUnion`	—	`List.Perm.kunion` `nodupKeys`
`singleton_entries` 📖	mathematical	—	`entries` `singleton`	—	—
`toAList_cons` 📖	mathematical	—	`List.toAList` `insert`	—	—
`union_assoc` 📖	mathematical	—	`entries` `AList` `instUnion`	—	`List.lookup_ext` `nodupKeys`
`union_comm_of_disjoint` 📖	mathematical	`Disjoint`	`entries` `AList` `instUnion`	—	`List.lookup_ext` `nodupKeys` `keys.eq_1` `List.dlookup_isSome`
`union_empty` 📖	mathematical	—	`AList` `instUnion` `instEmptyCollection`	—	`ext` `List.kunion_nil`
`union_entries` 📖	mathematical	—	`entries` `AList` `instUnion` `List.kunion`	—	—
`union_erase` 📖	mathematical	—	`erase` `AList` `instUnion`	—	`ext` `List.kunion_kerase`

List

Definitions

Name	Category	Theorems
`toAList` 📖	CompOp	3 math math: `AList.lookup_to_alist`, `AList.toAList_cons`, `AList.entries_toAList`

(root)

Definitions

Name	Category	Theorems
`AList` 📖	CompData	33 math math: `AList.mem_erase`, `AList.notMem_empty`, `AList.lookupFinsupp_eq_zero_iff`, `AList.union_erase`, `AList.insert_empty`, `AList.mem_keys`, `AList.empty_lookupFinsupp`, `AList.empty_union`, `AList.empty_entries`, `AList.mem_union`, `AList.mem_of_perm`, `AList.insertRec_empty`, `AList.perm_union`, `AList.union_comm_of_disjoint`, `AList.mem_replace`, `AList.mem_insert`, `AList.mem_lookup_union`, `Finsupp.mem_toAlist`, `Finmap.empty_toFinmap`, `AList.insert_union`, `AList.extract_eq_lookup_erase`, `AList.mem_mk`, `AList.union_assoc`, `AList.lookup_empty`, `Finmap.union_toFinmap`, `AList.lookup_isSome`, `AList.union_entries`, `AList.keys_empty`, `AList.lookupFinsupp_surjective`, `AList.lookup_union_eq_some`, `AList.lookup_eq_none`, `Finmap.mem_toFinmap`, `AList.union_empty`

---

← Back to Index