Sigma

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

Statistics

Metric	Count
Definitions `NodupKeys`, `dedupKeys`, `dlookup`, `kerase`, `kextract`, `keys`, `kinsert`, `kreplace`, `kunion`, `lookupAll`	10
Theorems `eq_of_fst_eq`, `eq_of_mk_mem`, `kerase`, `kunion`, `map₁`, `map₂`, `nodup`, `pairwise_ne`, `sublist`, `kerase`, `kinsert`, `kreplace`, `kunion`, `kunion_left`, `kunion_right`, `dedupKeys_cons`, `dlookup_append`, `dlookup_cons_eq`, `dlookup_cons_ne`, `dlookup_dedupKeys`, `dlookup_eq_none`, `dlookup_isSome`, `dlookup_kerase`, `dlookup_kerase_ne`, `dlookup_kinsert`, `dlookup_kinsert_ne`, `dlookup_kunion_eq_some`, `dlookup_kunion_left`, `dlookup_kunion_right`, `dlookup_map`, `dlookup_map₁`, `dlookup_map₂`, `dlookup_nil`, `exists_of_kerase`, `exists_of_mem_keys`, `head?_lookupAll`, `kerase_append_left`, `kerase_append_right`, `kerase_comm`, `kerase_cons_eq`, `kerase_cons_ne`, `kerase_kerase`, `kerase_keys_subset`, `kerase_nil`, `kerase_of_notMem_keys`, `kerase_sublist`, `kextract_eq_dlookup_kerase`, `keys_append`, `keys_cons`, `keys_kerase`, `keys_kreplace`, `keys_nil`, `kinsert_def`, `kinsert_nodupKeys`, `kreplace_nodupKeys`, `kreplace_of_forall_not`, `kreplace_self`, `kunion_cons`, `kunion_kerase`, `kunion_nil`, `lookupAll_cons_eq`, `lookupAll_cons_ne`, `lookupAll_eq_dlookup`, `lookupAll_eq_nil`, `lookupAll_length_le_one`, `lookupAll_nil`, `lookupAll_nodup`, `lookupAll_sublist`, `lookup_ext`, `map_dlookup_eq_find`, `map₂_keys`, `mem_dlookup`, `mem_dlookup_iff`, `mem_dlookup_kunion`, `mem_dlookup_kunion_middle`, `mem_ext`, `mem_keys`, `mem_keys_kerase_of_ne`, `mem_keys_kinsert`, `mem_keys_kunion`, `mem_keys_of_mem`, `mem_keys_of_mem_keys_kerase`, `mem_lookupAll`, `ne_key`, `nil_kunion`, `nodupKeys_cons`, `nodupKeys_dedupKeys`, `nodupKeys_flatten`, `nodupKeys_iff_pairwise`, `nodupKeys_middle`, `nodupKeys_nil`, `nodupKeys_of_nodupKeys_cons`, `nodupKeys_singleton`, `nodup_zipIdx_map_snd`, `notMem_keys`, `notMem_keys_kerase`, `notMem_keys_of_nodupKeys_cons`, `of_mem_dlookup`, `perm_dlookup`, `perm_lookupAll`, `perm_nodupKeys`, `sizeOf_dedupKeys`, `sizeOf_kerase`, `sublist_dlookup`	104
Total	114

List

Definitions

Name	Category	Theorems
`NodupKeys` 📖	MathDef	12 math math: `nodupKeys_middle`, `perm_nodupKeys`, `nodupKeys_cons`, `nodupKeys_flatten`, `kreplace_nodupKeys`, `nodupKeys_singleton`, `nodupKeys_dedupKeys`, `Multiset.coe_nodupKeys`, `nodupKeys_iff_pairwise`, `AList.insert_of_notMem`, `nodupKeys_nil`, `AList.nodupKeys`
`dedupKeys` 📖	CompOp	5 math math: `dedupKeys_cons`, `dlookup_dedupKeys`, `nodupKeys_dedupKeys`, `sizeOf_dedupKeys`, `AList.entries_toAList`
`dlookup` 📖	CompOp	27 math math: `Finmap.dlookup_list_toFinmap`, `dlookup_kerase`, `dlookup_map₁`, `dlookup_map₂`, `dlookup_dedupKeys`, `dlookup_eq_none`, `map_dlookup_eq_find`, `lookupAll_eq_dlookup`, `perm_dlookup`, `dlookup_map`, `dlookup_kerase_ne`, `mem_dlookup_kunion`, `dlookup_cons_ne`, `kextract_eq_dlookup_kerase`, `dlookup_kunion_left`, `AList.lookup_to_alist`, `mem_dlookup`, `dlookup_isSome`, `dlookup_append`, `dlookup_kunion_right`, `dlookup_cons_eq`, `mem_dlookup_iff`, `head?_lookupAll`, `dlookup_kunion_eq_some`, `dlookup_kinsert_ne`, `dlookup_kinsert`, `dlookup_nil`
`kerase` 📖	CompOp	24 math math: `kerase_nil`, `exists_of_kerase`, `dlookup_kerase`, `kerase_comm`, `Perm.kerase`, `kerase_of_notMem_keys`, `dlookup_kerase_ne`, `kerase_append_right`, `kerase_cons_ne`, `kerase_sublist`, `mem_keys_kerase_of_ne`, `kinsert_def`, `AList.entries_insert`, `kextract_eq_dlookup_kerase`, `kerase_cons_eq`, `NodupKeys.kerase`, `kunion_kerase`, `keys_kerase`, `kerase_append_left`, `sizeOf_kerase`, `kerase_keys_subset`, `kerase_kerase`, `kunion_cons`, `notMem_keys_kerase`
`kextract` 📖	CompOp	1 math math: `kextract_eq_dlookup_kerase`
`keys` 📖	CompOp	27 math math: `mem_keys_of_mem`, `keys_cons`, `keys_nil`, `dlookup_eq_none`, `nodupKeys_cons`, `nodupKeys_flatten`, `keys_append`, `mem_dlookup_kunion`, `keys_kreplace`, `ne_key`, `Multiset.coe_keys`, `mem_keys_kunion`, `mem_keys_kerase_of_ne`, `AList.lookupFinsupp_support`, `notMem_keys`, `keys_kerase`, `dlookup_isSome`, `kerase_keys_subset`, `AList.mem_mk`, `AList.insert_of_notMem`, `dlookup_kunion_eq_some`, `mem_keys`, `AList.keys_mk`, `notMem_keys_kerase`, `map₂_keys`, `mem_keys_kinsert`, `notMem_keys_of_nodupKeys_cons`
`kinsert` 📖	CompOp	7 math math: `dedupKeys_cons`, `kinsert_nodupKeys`, `kinsert_def`, `Perm.kinsert`, `dlookup_kinsert_ne`, `mem_keys_kinsert`, `dlookup_kinsert`
`kreplace` 📖	CompOp	5 math math: `kreplace_nodupKeys`, `keys_kreplace`, `kreplace_of_forall_not`, `kreplace_self`, `Perm.kreplace`
`kunion` 📖	CompOp	14 math math: `mem_dlookup_kunion`, `NodupKeys.kunion`, `Perm.kunion_left`, `mem_keys_kunion`, `dlookup_kunion_left`, `Perm.kunion_right`, `Perm.kunion`, `kunion_kerase`, `nil_kunion`, `dlookup_kunion_right`, `kunion_cons`, `dlookup_kunion_eq_some`, `kunion_nil`, `AList.union_entries`
`lookupAll` 📖	CompOp	11 math math: `lookupAll_sublist`, `perm_lookupAll`, `mem_lookupAll`, `lookupAll_cons_ne`, `lookupAll_eq_dlookup`, `lookupAll_length_le_one`, `lookupAll_nil`, `lookupAll_nodup`, `lookupAll_eq_nil`, `lookupAll_cons_eq`, `head?_lookupAll`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dedupKeys_cons` 📖	mathematical	—	`dedupKeys` `kinsert`	—	—
`dlookup_append` 📖	mathematical	—	`dlookup`	—	—
`dlookup_cons_eq` 📖	mathematical	—	`dlookup`	—	—
`dlookup_cons_ne` 📖	mathematical	—	`dlookup`	—	—
`dlookup_dedupKeys` 📖	mathematical	—	`dlookup` `dedupKeys`	—	`dedupKeys_cons` `dlookup_kinsert` `dlookup_cons_eq` `dlookup_kinsert_ne` `dlookup_cons_ne`
`dlookup_eq_none` 📖	mathematical	—	`dlookup` `keys`	—	—
`dlookup_isSome` 📖	mathematical	—	`dlookup` `keys`	—	—
`dlookup_kerase` 📖	mathematical	`NodupKeys`	`dlookup` `kerase`	—	`dlookup_eq_none` `notMem_keys_kerase`
`dlookup_kerase_ne` 📖	mathematical	—	`dlookup` `kerase`	—	`dlookup.congr_simp` `kerase_cons_ne` `dlookup_cons_eq` `kerase_cons_eq` `dlookup_cons_ne`
`dlookup_kinsert` 📖	mathematical	—	`dlookup` `kinsert`	—	`dlookup_cons_eq`
`dlookup_kinsert_ne` 📖	mathematical	—	`dlookup` `kinsert`	—	`dlookup_cons_ne` `dlookup_kerase_ne`
`dlookup_kunion_eq_some` 📖	mathematical	—	`dlookup` `kunion` `keys`	—	`mem_dlookup_kunion`
`dlookup_kunion_left` 📖	mathematical	`keys`	`dlookup` `kunion`	—	`dlookup_cons_eq` `kunion_cons` `dlookup_cons_ne`
`dlookup_kunion_right` 📖	mathematical	`keys`	`dlookup` `kunion`	—	`dlookup_cons_ne` `dlookup_kerase_ne`
`dlookup_map` 📖	mathematical	—	`dlookup` `Sigma.map`	—	—
`dlookup_map₁` 📖	mathematical	—	`dlookup` `Sigma.map`	—	`dlookup_map`
`dlookup_map₂` 📖	mathematical	—	`dlookup` `Sigma.map`	—	`dlookup_map`
`dlookup_nil` 📖	mathematical	—	`dlookup`	—	—
`exists_of_kerase` 📖	mathematical	`keys`	`kerase`	—	`kerase_cons_eq` `kerase_cons_ne`
`exists_of_mem_keys` 📖	—	`keys`	—	—	—
`head?_lookupAll` 📖	mathematical	—	`lookupAll` `dlookup`	—	`lookupAll_cons_eq` `dlookup_cons_eq` `lookupAll_cons_ne` `dlookup_cons_ne`
`kerase_append_left` 📖	mathematical	`keys`	`kerase`	—	`kerase_cons_eq` `kerase_cons_ne`
`kerase_append_right` 📖	mathematical	`keys`	`kerase`	—	`kerase_cons_ne`
`kerase_comm` 📖	mathematical	—	`kerase`	—	`exists_of_kerase` `kerase_append_left` `kerase_append_right` `mem_keys_kerase_of_ne` `kerase_cons_eq` `kerase_cons_ne` `kerase_of_notMem_keys` `mem_keys_of_mem_keys_kerase`
`kerase_cons_eq` 📖	mathematical	—	`kerase`	—	—
`kerase_cons_ne` 📖	mathematical	—	`kerase`	—	—
`kerase_kerase` 📖	mathematical	—	`kerase`	—	`kerase_cons_eq` `kerase_cons_ne`
`kerase_keys_subset` 📖	mathematical	—	`keys` `kerase`	—	`kerase_sublist`
`kerase_nil` 📖	mathematical	—	`kerase`	—	—
`kerase_of_notMem_keys` 📖	mathematical	`keys`	`kerase`	—	`kerase_cons_ne`
`kerase_sublist` 📖	mathematical	—	`kerase`	—	—
`kextract_eq_dlookup_kerase` 📖	mathematical	—	`kextract` `dlookup` `kerase`	—	`dlookup_cons_eq` `dlookup_cons_ne`
`keys_append` 📖	mathematical	—	`keys`	—	—
`keys_cons` 📖	mathematical	—	`keys`	—	—
`keys_kerase` 📖	mathematical	—	`keys` `kerase`	—	`keys.eq_1` `kerase.eq_1`
`keys_kreplace` 📖	mathematical	—	`keys` `kreplace`	—	`lookmap_map_eq` `instIsEmptyFalse`
`keys_nil` 📖	mathematical	—	`keys`	—	—
`kinsert_def` 📖	mathematical	—	`kinsert` `kerase`	—	—
`kinsert_nodupKeys` 📖	mathematical	`NodupKeys`	`kinsert`	—	`nodupKeys_cons` `notMem_keys_kerase` `NodupKeys.kerase`
`kreplace_nodupKeys` 📖	mathematical	—	`NodupKeys` `kreplace`	—	`keys_kreplace`
`kreplace_of_forall_not` 📖	mathematical	—	`kreplace`	—	`lookmap_of_forall_not`
`kreplace_self` 📖	mathematical	`NodupKeys`	`kreplace`	—	`lookmap_congr` `NodupKeys.eq_of_mk_mem` `lookmap_id'`
`kunion_cons` 📖	mathematical	—	`kunion` `kerase`	—	—
`kunion_kerase` 📖	mathematical	—	`kunion` `kerase`	—	`kerase_cons_eq` `kerase_cons_ne` `kerase_comm`
`kunion_nil` 📖	mathematical	—	`kunion`	—	`kunion.eq_2` `kerase_nil`
`lookupAll_cons_eq` 📖	mathematical	—	`lookupAll`	—	—
`lookupAll_cons_ne` 📖	mathematical	—	`lookupAll`	—	—
`lookupAll_eq_dlookup` 📖	mathematical	`NodupKeys`	`lookupAll` `dlookup`	—	`head?_lookupAll` `lookupAll_length_le_one`
`lookupAll_eq_nil` 📖	mathematical	—	`lookupAll`	—	`lookupAll_cons_eq` `instIsEmptyFalse` `lookupAll_cons_ne`
`lookupAll_length_le_one` 📖	mathematical	`NodupKeys`	`lookupAll`	—	`lookupAll_sublist`
`lookupAll_nil` 📖	mathematical	—	`lookupAll`	—	—
`lookupAll_nodup` 📖	mathematical	`NodupKeys`	`lookupAll`	—	`lookupAll_eq_dlookup` `Option.toList_nodup`
`lookupAll_sublist` 📖	mathematical	—	`lookupAll`	—	`lookupAll_cons_eq` `lookupAll_cons_ne`
`lookup_ext` 📖	—	`NodupKeys` `dlookup`	—	—	—
`map_dlookup_eq_find` 📖	mathematical	—	`dlookup`	—	—
`map₂_keys` 📖	mathematical	—	`keys` `Sigma.map`	—	—
`mem_dlookup` 📖	mathematical	`NodupKeys`	`dlookup`	—	`dlookup_isSome` `mem_keys_of_mem` `NodupKeys.eq_of_mk_mem` `of_mem_dlookup`
`mem_dlookup_iff` 📖	mathematical	`NodupKeys`	`dlookup`	—	`of_mem_dlookup` `mem_dlookup`
`mem_dlookup_kunion` 📖	mathematical	—	`dlookup` `kunion` `keys`	—	`dlookup_cons_eq` `dlookup_cons_ne` `dlookup_kerase_ne`
`mem_dlookup_kunion_middle` 📖	—	`dlookup` `kunion` `keys`	—	—	`mem_dlookup_kunion` `mem_keys_kunion`
`mem_ext` 📖	—	—	—	—	—
`mem_keys` 📖	mathematical	—	`keys`	—	`exists_of_mem_keys` `mem_keys_of_mem`
`mem_keys_kerase_of_ne` 📖	mathematical	—	`keys` `kerase`	—	`mem_keys_of_mem_keys_kerase` `exists_of_kerase` `kerase_of_notMem_keys`
`mem_keys_kinsert` 📖	mathematical	—	`keys` `kinsert`	—	—
`mem_keys_kunion` 📖	mathematical	—	`keys` `kunion`	—	—
`mem_keys_of_mem` 📖	mathematical	—	`keys`	—	—
`mem_keys_of_mem_keys_kerase` 📖	—	`keys` `kerase`	—	—	`kerase_keys_subset`
`mem_lookupAll` 📖	mathematical	—	`lookupAll`	—	`lookupAll_cons_eq` `lookupAll_cons_ne`
`ne_key` 📖	mathematical	—	`keys`	—	—
`nil_kunion` 📖	mathematical	—	`kunion`	—	—
`nodupKeys_cons` 📖	mathematical	—	`NodupKeys` `keys`	—	—
`nodupKeys_dedupKeys` 📖	mathematical	—	`NodupKeys` `dedupKeys`	—	`keys_kerase` `NodupKeys.kerase`
`nodupKeys_flatten` 📖	mathematical	—	`NodupKeys` `keys`	—	`nodupKeys_iff_pairwise`
`nodupKeys_iff_pairwise` 📖	mathematical	—	`NodupKeys`	—	—
`nodupKeys_middle` 📖	mathematical	—	`NodupKeys`	—	—
`nodupKeys_nil` 📖	mathematical	—	`NodupKeys`	—	—
`nodupKeys_of_nodupKeys_cons` 📖	—	`NodupKeys`	—	—	`nodupKeys_cons`
`nodupKeys_singleton` 📖	mathematical	—	`NodupKeys`	—	`nodup_singleton`
`nodup_zipIdx_map_snd` 📖	—	—	—	—	—
`notMem_keys` 📖	mathematical	—	`keys`	—	—
`notMem_keys_kerase` 📖	mathematical	`NodupKeys`	`keys` `kerase`	—	`kerase_of_notMem_keys` `kerase_cons_eq` `kerase_cons_ne`
`notMem_keys_of_nodupKeys_cons` 📖	mathematical	`NodupKeys`	`keys`	—	—
`of_mem_dlookup` 📖	—	`dlookup`	—	—	—
`perm_dlookup` 📖	mathematical	`NodupKeys`	`dlookup`	—	`perm_nodupKeys` `mem_dlookup_iff`
`perm_lookupAll` 📖	mathematical	`NodupKeys`	`lookupAll`	—	`perm_nodupKeys` `lookupAll_eq_dlookup` `perm_dlookup`
`perm_nodupKeys` 📖	mathematical	—	`NodupKeys`	—	—
`sizeOf_dedupKeys` 📖	mathematical	—	`dedupKeys`	—	`Sigma.eta` `sizeOf_kerase`
`sizeOf_kerase` 📖	mathematical	—	`kerase`	—	`kerase_of_notMem_keys` `kerase_cons_eq` `kerase_cons_ne`
`sublist_dlookup` 📖	—	`NodupKeys` `dlookup`	—	—	—

List.NodupKeys

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_fst_eq` 📖	—	`List.NodupKeys`	—	—	`List.Pairwise.forall_of_forall` `List.nodupKeys_iff_pairwise`
`eq_of_mk_mem` 📖	—	`List.NodupKeys`	—	—	—
`kerase` 📖	mathematical	`List.NodupKeys`	`List.kerase`	—	`sublist` `List.kerase_sublist`
`kunion` 📖	mathematical	`List.NodupKeys`	`List.kunion`	—	`kerase`
`map₁` 📖	mathematical	`List.NodupKeys`	`Sigma.map`	—	`List.dlookup_map₁`
`map₂` 📖	mathematical	`List.NodupKeys`	`Sigma.map`	—	`List.map₂_keys`
`nodup` 📖	—	`List.NodupKeys`	—	—	`List.Nodup.of_map`
`pairwise_ne` 📖	—	`List.NodupKeys`	—	—	`List.nodupKeys_iff_pairwise`
`sublist` 📖	—	`List.NodupKeys`	—	—	—

List.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`kerase` 📖	mathematical	`List.NodupKeys`	`List.kerase`	—	`List.nodupKeys_iff_pairwise`
`kinsert` 📖	mathematical	`List.NodupKeys`	`List.kinsert`	—	`kerase`
`kreplace` 📖	mathematical	`List.NodupKeys`	`List.kreplace`	—	`List.perm_lookmap` `List.NodupKeys.pairwise_ne`
`kunion` 📖	mathematical	`List.NodupKeys`	`List.kunion`	—	`kunion_right` `kunion_left`
`kunion_left` 📖	mathematical	`List.NodupKeys`	`List.kunion`	—	`List.NodupKeys.kerase` `kerase`
`kunion_right` 📖	mathematical	—	`List.kunion`	—	`List.kerase_comm`

---

← Back to Index