Finmap

Statistics

Metric	Count
Definitions `toFinmap`, `Finmap`, `all`, `any`, `decidableEq`, `entries`, `erase`, `extract`, `foldl`, `insert`, `instDecidableMem`, `instDecidableRelDisjoint`, `instEmptyCollection`, `instInhabited`, `instMembership`, `instSDiff`, `instUnion`, `keys`, `keysLookupEquiv`, `liftOn`, `liftOn₂`, `lookup`, `replace`, `sdiff`, `singleton`, `union`, `toFinmap`, `NodupKeys`, `keys`	29
Theorems `toFinmap_entries`, `toFinmap_eq`, `symm_iff`, `disjoint_empty`, `disjoint_union_left`, `disjoint_union_right`, `dlookup_list_toFinmap`, `empty_toFinmap`, `empty_union`, `entries_insert_of_notMem`, `erase_erase`, `erase_toFinmap`, `erase_union_singleton`, `ext`, `ext_iff`, `ext_iff'`, `ext_lookup`, `extract_eq_lookup_erase`, `induction_on`, `induction_on₂`, `induction_on₃`, `insert_insert`, `insert_insert_of_ne`, `insert_singleton_eq`, `insert_toFinmap`, `insert_union`, `keysLookupEquiv_apply_coe_fst`, `keysLookupEquiv_apply_coe_snd`, `keysLookupEquiv_symm_apply_keys`, `keysLookupEquiv_symm_apply_lookup`, `keys_empty`, `keys_erase`, `keys_erase_toFinset`, `keys_ext`, `keys_replace`, `keys_singleton`, `keys_union`, `keys_val`, `liftOn_toFinmap`, `liftOn₂_toFinmap`, `lookup_empty`, `lookup_eq_none`, `lookup_eq_some_iff`, `lookup_erase`, `lookup_erase_ne`, `lookup_insert`, `lookup_insert_of_ne`, `lookup_isSome`, `lookup_singleton_eq`, `lookup_toFinmap`, `lookup_union_left`, `lookup_union_left_of_not_in`, `lookup_union_right`, `mem_def`, `mem_erase`, `mem_iff`, `mem_insert`, `mem_keys`, `mem_list_toFinmap`, `mem_lookup_iff`, `mem_lookup_union`, `mem_lookup_union'`, `mem_lookup_union_middle`, `mem_of_lookup_eq_some`, `mem_replace`, `mem_singleton`, `mem_toFinmap`, `mem_union`, `nodupKeys`, `nodup_entries`, `notMem_empty`, `notMem_erase_self`, `replace_toFinmap`, `sigma_keys_lookup`, `toFinmap_cons`, `toFinmap_nil`, `union_assoc`, `union_cancel`, `union_comm_of_disjoint`, `union_empty`, `union_toFinmap`, `nodup`, `nodup_keys`, `coe_keys`, `coe_nodupKeys`, `keys_cons`, `keys_singleton`, `keys_zero`, `nodup_keys`	89
Total	118

AList

Definitions

Name	Category	Theorems
`toFinmap` 📖	CompOp	14 math math: `toFinmap_entries`, `toFinmap_eq`, `Finmap.keys_ext`, `Finmap.empty_toFinmap`, `Finmap.liftOn₂_toFinmap`, `Finmap.insert_toFinmap`, `Finmap.keys_val`, `Finmap.keys_erase_toFinset`, `Finmap.erase_toFinmap`, `Finmap.replace_toFinmap`, `Finmap.union_toFinmap`, `Finmap.liftOn_toFinmap`, `Finmap.lookup_toFinmap`, `Finmap.mem_toFinmap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFinmap_entries` 📖	mathematical	—	`Finmap.entries` `toFinmap` `Multiset.ofList` `entries`	—	—
`toFinmap_eq` 📖	mathematical	—	`toFinmap` `entries`	—	`nodupKeys`

Finmap

Definitions

Name	Category	Theorems
`all` 📖	CompOp	—
`any` 📖	CompOp	—
`decidableEq` 📖	CompOp	—
`entries` 📖	CompOp	10 math math: `lookup_eq_some_iff`, `AList.toFinmap_entries`, `nodup_entries`, `entries_insert_of_notMem`, `ext_iff`, `ext_iff'`, `mem_def`, `sigma_keys_lookup`, `nodupKeys`, `mem_lookup_iff`
`erase` 📖	CompOp	9 math math: `lookup_erase`, `mem_erase`, `keys_erase`, `lookup_erase_ne`, `notMem_erase_self`, `erase_toFinmap`, `extract_eq_lookup_erase`, `erase_union_singleton`, `erase_erase`
`extract` 📖	CompOp	1 math math: `extract_eq_lookup_erase`
`foldl` 📖	CompOp	—
`insert` 📖	CompOp	10 math math: `lookup_insert_of_ne`, `insert_insert_of_ne`, `entries_insert_of_notMem`, `toFinmap_cons`, `lookup_insert`, `insert_singleton_eq`, `insert_toFinmap`, `insert_union`, `mem_insert`, `insert_insert`
`instDecidableMem` 📖	CompOp	—
`instDecidableRelDisjoint` 📖	CompOp	—
`instEmptyCollection` 📖	CompOp	8 math math: `lookup_empty`, `disjoint_empty`, `notMem_empty`, `empty_toFinmap`, `toFinmap_nil`, `keys_empty`, `empty_union`, `union_empty`
`instInhabited` 📖	CompOp	—
`instMembership` 📖	CompOp	17 math math: `mem_erase`, `mem_singleton`, `mem_replace`, `mem_def`, `mem_iff`, `mem_of_lookup_eq_some`, `notMem_empty`, `lookup_isSome`, `mem_lookup_union`, `mem_lookup_union'`, `mem_keys`, `notMem_erase_self`, `mem_union`, `lookup_eq_none`, `mem_list_toFinmap`, `mem_insert`, `mem_toFinmap`
`instSDiff` 📖	CompOp	—
`instUnion` 📖	CompOp	17 math math: `union_assoc`, `union_cancel`, `union_comm_of_disjoint`, `disjoint_union_right`, `lookup_union_left_of_not_in`, `disjoint_union_left`, `insert_union`, `mem_lookup_union`, `lookup_union_left`, `mem_lookup_union'`, `keys_union`, `mem_union`, `union_toFinmap`, `lookup_union_right`, `erase_union_singleton`, `empty_union`, `union_empty`
`keys` 📖	CompOp	12 math math: `keys_ext`, `sigma_keys_lookup`, `keys_singleton`, `keys_erase`, `keysLookupEquiv_symm_apply_keys`, `keys_val`, `mem_keys`, `keys_erase_toFinset`, `keys_union`, `keys_replace`, `keys_empty`, `keysLookupEquiv_apply_coe_fst`
`keysLookupEquiv` 📖	CompOp	4 math math: `keysLookupEquiv_apply_coe_snd`, `keysLookupEquiv_symm_apply_keys`, `keysLookupEquiv_symm_apply_lookup`, `keysLookupEquiv_apply_coe_fst`
`liftOn` 📖	CompOp	1 math math: `liftOn_toFinmap`
`liftOn₂` 📖	CompOp	1 math math: `liftOn₂_toFinmap`
`lookup` 📖	CompOp	22 math math: `lookup_singleton_eq`, `lookup_erase`, `lookup_eq_some_iff`, `dlookup_list_toFinmap`, `lookup_insert_of_ne`, `lookup_empty`, `lookup_insert`, `mem_iff`, `sigma_keys_lookup`, `lookup_union_left_of_not_in`, `mem_lookup_iff`, `keysLookupEquiv_apply_coe_snd`, `lookup_erase_ne`, `lookup_isSome`, `mem_lookup_union`, `lookup_union_left`, `mem_lookup_union'`, `lookup_eq_none`, `extract_eq_lookup_erase`, `keysLookupEquiv_symm_apply_lookup`, `lookup_union_right`, `lookup_toFinmap`
`replace` 📖	CompOp	3 math math: `mem_replace`, `keys_replace`, `replace_toFinmap`
`sdiff` 📖	CompOp	—
`singleton` 📖	CompOp	5 math math: `lookup_singleton_eq`, `mem_singleton`, `insert_singleton_eq`, `keys_singleton`, `erase_union_singleton`
`union` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_empty` 📖	mathematical	—	`Disjoint` `Finmap` `instEmptyCollection`	—	—
`disjoint_union_left` 📖	mathematical	—	`Disjoint` `Finmap` `instUnion`	—	—
`disjoint_union_right` 📖	mathematical	—	`Disjoint` `Finmap` `instUnion`	—	`Disjoint.symm_iff` `disjoint_union_left`
`dlookup_list_toFinmap` 📖	mathematical	—	`lookup` `List.toFinmap` `List.dlookup`	—	`List.toFinmap.eq_1` `lookup_toFinmap` `AList.lookup_to_alist`
`empty_toFinmap` 📖	mathematical	—	`AList.toFinmap` `AList` `AList.instEmptyCollection` `Finmap` `instEmptyCollection`	—	—
`empty_union` 📖	mathematical	—	`Finmap` `instUnion` `instEmptyCollection`	—	`induction_on` `empty_toFinmap` `union_toFinmap` `AList.empty_union`
`entries_insert_of_notMem` 📖	mathematical	`Finmap` `instMembership`	`entries` `insert` `Multiset.cons`	—	`induction_on` `insert_toFinmap` `AList.entries_insert_of_notMem` `mem_toFinmap`
`erase_erase` 📖	mathematical	—	`erase`	—	`induction_on` `ext` `erase_toFinmap` `AList.erase_erase`
`erase_toFinmap` 📖	mathematical	—	`erase` `AList.toFinmap` `AList.erase`	—	`liftOn_toFinmap`
`erase_union_singleton` 📖	mathematical	`lookup`	`Finmap` `instUnion` `erase` `singleton`	—	`ext_lookup` `lookup_union_right` `notMem_erase_self` `lookup_singleton_eq` `mem_singleton` `lookup_union_left_of_not_in` `lookup_erase_ne`
`ext` 📖	—	`entries`	—	—	—
`ext_iff` 📖	mathematical	—	`entries`	—	`ext`
`ext_iff'` 📖	mathematical	—	`entries`	—	`ext_iff`
`ext_lookup` 📖	—	`lookup`	—	—	`induction_on₂` `AList.toFinmap_eq` `List.lookup_ext` `AList.nodupKeys`
`extract_eq_lookup_erase` 📖	mathematical	—	`extract` `Finmap` `lookup` `erase`	—	`induction_on` `AList.extract_eq_lookup_erase` `liftOn.congr_simp` `liftOn_toFinmap` `erase_toFinmap`
`induction_on` 📖	—	`AList.toFinmap`	—	—	—
`induction_on₂` 📖	—	`AList.toFinmap`	—	—	`induction_on`
`induction_on₃` 📖	—	`AList.toFinmap`	—	—	`induction_on₂` `induction_on`
`insert_insert` 📖	mathematical	—	`insert`	—	`induction_on` `insert_toFinmap` `AList.insert_insert`
`insert_insert_of_ne` 📖	mathematical	—	`insert`	—	`induction_on` `insert_toFinmap` `AList.insert_insert_of_ne`
`insert_singleton_eq` 📖	mathematical	—	`insert` `singleton`	—	`insert_toFinmap` `AList.insert_singleton_eq`
`insert_toFinmap` 📖	mathematical	—	`insert` `AList.toFinmap` `AList.insert`	—	`liftOn_toFinmap`
`insert_union` 📖	mathematical	—	`insert` `Finmap` `instUnion`	—	`induction_on₂` `union_toFinmap` `insert_toFinmap` `AList.insert_union`
`keysLookupEquiv_apply_coe_fst` 📖	mathematical	—	`Finset` `DFunLike.coe` `Equiv` `Finmap` `EquivLike.toFunLike` `Equiv.instEquivLike` `keysLookupEquiv` `keys`	—	—
`keysLookupEquiv_apply_coe_snd` 📖	mathematical	—	`Finset` `DFunLike.coe` `Equiv` `Finmap` `EquivLike.toFunLike` `Equiv.instEquivLike` `keysLookupEquiv` `lookup`	—	—
`keysLookupEquiv_symm_apply_keys` 📖	mathematical	—	`keys` `DFunLike.coe` `Equiv` `Finset` `Finmap` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `keysLookupEquiv`	—	`Function.Surjective.forall` `Equiv.surjective` `Equiv.symm_apply_apply`
`keysLookupEquiv_symm_apply_lookup` 📖	mathematical	—	`lookup` `DFunLike.coe` `Equiv` `Finset` `Finmap` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `keysLookupEquiv`	—	`Function.Surjective.forall` `Equiv.surjective` `lookup.congr_simp` `Equiv.symm_apply_apply`
`keys_empty` 📖	mathematical	—	`keys` `Finmap` `instEmptyCollection` `Finset` `Finset.instEmptyCollection`	—	—
`keys_erase` 📖	mathematical	—	`keys` `erase` `Finset.erase`	—	`induction_on` `erase_toFinmap` `keys_erase_toFinset`
`keys_erase_toFinset` 📖	mathematical	—	`keys` `AList.toFinmap` `AList.erase` `Finset.erase`	—	`List.keys_kerase`
`keys_ext` 📖	mathematical	—	`keys` `AList.toFinmap` `AList.keys`	—	—
`keys_replace` 📖	mathematical	—	`keys` `replace`	—	`induction_on` `replace_toFinmap` `AList.keys_replace`
`keys_singleton` 📖	mathematical	—	`keys` `singleton` `Finset` `Finset.instSingleton`	—	—
`keys_union` 📖	mathematical	—	`keys` `Finmap` `instUnion` `Finset` `Finset.instUnion`	—	`induction_on₂` `Finset.ext` `union_toFinmap`
`keys_val` 📖	mathematical	—	`Finset.val` `keys` `AList.toFinmap` `Multiset.ofList` `AList.keys`	—	—
`liftOn_toFinmap` 📖	mathematical	—	`liftOn` `AList.toFinmap`	—	—
`liftOn₂_toFinmap` 📖	mathematical	—	`liftOn₂` `AList.toFinmap`	—	—
`lookup_empty` 📖	mathematical	—	`lookup` `Finmap` `instEmptyCollection`	—	—
`lookup_eq_none` 📖	mathematical	—	`lookup` `Finmap` `instMembership`	—	`induction_on` `AList.lookup_eq_none` `AList.perm_lookup`
`lookup_eq_some_iff` 📖	mathematical	—	`lookup` `Multiset` `Multiset.instMembership` `entries`	—	`mem_lookup_iff`
`lookup_erase` 📖	mathematical	—	`lookup` `erase`	—	`induction_on` `AList.lookup_erase`
`lookup_erase_ne` 📖	mathematical	—	`lookup` `erase`	—	`induction_on` `AList.lookup_erase_ne`
`lookup_insert` 📖	mathematical	—	`lookup` `insert`	—	`induction_on` `lookup.congr_simp` `insert_toFinmap` `AList.lookup_insert`
`lookup_insert_of_ne` 📖	mathematical	—	`lookup` `insert`	—	`induction_on` `lookup.congr_simp` `insert_toFinmap` `AList.lookup_insert_ne`
`lookup_isSome` 📖	mathematical	—	`lookup` `Finmap` `instMembership`	—	`induction_on` `AList.lookup_isSome` `AList.perm_lookup`
`lookup_singleton_eq` 📖	mathematical	—	`lookup` `singleton`	—	`singleton.eq_1` `lookup_toFinmap` `AList.singleton.eq_1` `AList.lookup.eq_1` `List.dlookup_cons_eq`
`lookup_toFinmap` 📖	mathematical	—	`lookup` `AList.toFinmap` `AList.lookup`	—	—
`lookup_union_left` 📖	mathematical	`Finmap` `instMembership`	`lookup` `instUnion`	—	`induction_on₂` `AList.lookup_union_left`
`lookup_union_left_of_not_in` 📖	mathematical	`Finmap` `instMembership`	`lookup` `instUnion`	—	`lookup_union_left` `lookup_union_right` `lookup_eq_none`
`lookup_union_right` 📖	mathematical	`Finmap` `instMembership`	`lookup` `instUnion`	—	`induction_on₂` `AList.lookup_union_right`
`mem_def` 📖	mathematical	—	`Finmap` `instMembership` `Multiset` `Multiset.instMembership` `Multiset.keys` `entries`	—	—
`mem_erase` 📖	mathematical	—	`Finmap` `instMembership` `erase`	—	`induction_on` `erase_toFinmap`
`mem_iff` 📖	mathematical	—	`Finmap` `instMembership` `lookup`	—	`induction_on` `List.mem_keys` `List.mem_dlookup_iff` `AList.nodupKeys`
`mem_insert` 📖	mathematical	—	`Finmap` `instMembership` `insert`	—	`induction_on` `AList.mem_insert`
`mem_keys` 📖	mathematical	—	`Finset` `Finset.instMembership` `keys` `Finmap` `instMembership`	—	`induction_on` `AList.mem_keys`
`mem_list_toFinmap` 📖	mathematical	—	`Finmap` `instMembership` `List.toFinmap`	—	—
`mem_lookup_iff` 📖	mathematical	—	`lookup` `Multiset` `Multiset.instMembership` `entries`	—	`List.mem_dlookup_iff` `AList.perm_lookup`
`mem_lookup_union` 📖	mathematical	—	`lookup` `Finmap` `instUnion` `instMembership`	—	`induction_on₂` `AList.mem_lookup_union`
`mem_lookup_union'` 📖	mathematical	—	`lookup` `Finmap` `instUnion` `instMembership`	—	`induction_on₂` `AList.mem_lookup_union`
`mem_lookup_union_middle` 📖	—	`lookup` `Finmap` `instUnion` `instMembership`	—	—	`induction_on₃` `AList.mem_lookup_union_middle`
`mem_of_lookup_eq_some` 📖	mathematical	`lookup`	`Finmap` `instMembership`	—	`mem_iff`
`mem_replace` 📖	mathematical	—	`Finmap` `instMembership` `replace`	—	`induction_on` `replace_toFinmap`
`mem_singleton` 📖	mathematical	—	`Finmap` `instMembership` `singleton`	—	—
`mem_toFinmap` 📖	mathematical	—	`Finmap` `instMembership` `AList.toFinmap` `AList` `AList.instMembership`	—	—
`mem_union` 📖	mathematical	—	`Finmap` `instMembership` `instUnion`	—	`induction_on₂` `AList.mem_union`
`nodupKeys` 📖	mathematical	—	`Multiset.NodupKeys` `entries`	—	—
`nodup_entries` 📖	mathematical	—	`Multiset.Nodup` `entries`	—	`Multiset.NodupKeys.nodup` `nodupKeys`
`notMem_empty` 📖	mathematical	—	`Finmap` `instMembership` `instEmptyCollection`	—	`Multiset.notMem_zero`
`notMem_erase_self` 📖	mathematical	—	`Finmap` `instMembership` `erase`	—	`mem_erase` `not_and_or`
`replace_toFinmap` 📖	mathematical	—	`replace` `AList.toFinmap` `AList.replace`	—	`liftOn_toFinmap`
`sigma_keys_lookup` 📖	mathematical	—	`Finset.sigma` `keys` `Option.toFinset` `lookup` `entries` `nodup_entries`	—	`Finset.ext` `nodup_entries` `Multiset.mem_map_of_mem` `Sigma.eta`
`toFinmap_cons` 📖	mathematical	—	`List.toFinmap` `insert`	—	—
`toFinmap_nil` 📖	mathematical	—	`List.toFinmap` `Finmap` `instEmptyCollection`	—	—
`union_assoc` 📖	mathematical	—	`Finmap` `instUnion`	—	`induction_on₃` `union_toFinmap`
`union_cancel` 📖	mathematical	`Disjoint`	`Finmap` `instUnion`	—	`ext_lookup` `lookup_union_left_of_not_in` `lookup_union_left` `lookup_eq_none`
`union_comm_of_disjoint` 📖	mathematical	`Disjoint`	`Finmap` `instUnion`	—	`induction_on₂` `union_toFinmap` `AList.union_comm_of_disjoint`
`union_empty` 📖	mathematical	—	`Finmap` `instUnion` `instEmptyCollection`	—	`induction_on` `empty_toFinmap` `union_toFinmap` `AList.union_empty`
`union_toFinmap` 📖	mathematical	—	`Finmap` `instUnion` `AList.toFinmap` `AList` `AList.instUnion`	—	—

Finmap.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symm_iff` 📖	mathematical	—	`Finmap.Disjoint`	—	`symm`

List

Definitions

Name	Category	Theorems
`toFinmap` 📖	CompOp	4 math math: `Finmap.dlookup_list_toFinmap`, `Finmap.toFinmap_cons`, `Finmap.toFinmap_nil`, `Finmap.mem_list_toFinmap`

Multiset

Definitions

Name	Category	Theorems
`NodupKeys` 📖	MathDef	3 math math: `nodup_keys`, `Finmap.nodupKeys`, `coe_nodupKeys`
`keys` 📖	CompOp	7 math math: `nodup_keys`, `keys_zero`, `keys_singleton`, `Finmap.mem_def`, `coe_keys`, `NodupKeys.nodup_keys`, `keys_cons`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_keys` 📖	mathematical	—	`keys` `ofList` `List.keys`	—	—
`coe_nodupKeys` 📖	mathematical	—	`NodupKeys` `ofList` `List.NodupKeys`	—	—
`keys_cons` 📖	mathematical	—	`keys` `cons`	—	`map_cons`
`keys_singleton` 📖	mathematical	—	`keys` `Multiset` `instSingleton`	—	—
`keys_zero` 📖	mathematical	—	`keys` `Multiset` `instZero`	—	—
`nodup_keys` 📖	mathematical	—	`Nodup` `keys` `NodupKeys`	—	—

Multiset.NodupKeys

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nodup` 📖	mathematical	`Multiset.NodupKeys`	`Multiset.Nodup`	—	`Multiset.Nodup.of_map` `nodup_keys`
`nodup_keys` 📖	mathematical	`Multiset.NodupKeys`	`Multiset.Nodup` `Multiset.keys`	—	`Multiset.nodup_keys`

(root)

Definitions

Name	Category	Theorems
`Finmap` 📖	CompData	38 math math: `Finmap.mem_erase`, `Finmap.union_assoc`, `Finmap.union_cancel`, `Finmap.mem_singleton`, `Finmap.mem_replace`, `Finmap.lookup_empty`, `Finmap.union_comm_of_disjoint`, `Finmap.mem_def`, `Finmap.mem_iff`, `Finmap.mem_of_lookup_eq_some`, `Finmap.disjoint_union_right`, `Finmap.disjoint_empty`, `Finmap.disjoint_union_left`, `Finmap.notMem_empty`, `Finmap.keysLookupEquiv_apply_coe_snd`, `Finmap.keysLookupEquiv_symm_apply_keys`, `Finmap.empty_toFinmap`, `Finmap.lookup_isSome`, `Finmap.insert_union`, `Finmap.toFinmap_nil`, `Finmap.mem_lookup_union`, `Finmap.mem_lookup_union'`, `Finmap.mem_keys`, `Finmap.notMem_erase_self`, `Finmap.keys_union`, `Finmap.mem_union`, `Finmap.lookup_eq_none`, `Finmap.union_toFinmap`, `Finmap.extract_eq_lookup_erase`, `Finmap.keysLookupEquiv_symm_apply_lookup`, `Finmap.erase_union_singleton`, `Finmap.mem_list_toFinmap`, `Finmap.keys_empty`, `Finmap.empty_union`, `Finmap.mem_insert`, `Finmap.keysLookupEquiv_apply_coe_fst`, `Finmap.mem_toFinmap`, `Finmap.union_empty`

---

← Back to Index