# Documentation

Mathlib.Data.Finmap

# Finite maps over Multiset#

### Multisets of sigma types #

def Multiset.keys {α : Type u} {β : αType v} (s : Multiset ()) :

Multiset of keys of an association multiset.

Instances For
@[simp]
theorem Multiset.coe_keys {α : Type u} {β : αType v} {l : List ()} :
= ↑()
def Multiset.NodupKeys {α : Type u} {β : αType v} (s : Multiset ()) :

NodupKeys s means that s has no duplicate keys.

Instances For
@[simp]
theorem Multiset.coe_nodupKeys {α : Type u} {β : αType v} {l : List ()} :
theorem Multiset.nodup_keys {α : Type u} {β : αType v} {m : Multiset ((a : α) × β a)} :
theorem Multiset.NodupKeys.nodup_keys {α : Type u} {β : αType v} {m : Multiset ((a : α) × β a)} :

Alias of the reverse direction of Multiset.nodup_keys.

theorem Multiset.NodupKeys.nodup {α : Type u} {β : αType v} {m : Multiset ((a : α) × β a)} (h : ) :

### Finmap #

structure Finmap {α : Type u} (β : αType v) :
Type (max u v)
• entries : Multiset ()

The underlying Multiset of a Finmap

• nodupKeys : Multiset.NodupKeys s.entries

There are no duplicate keys in entries

Finmap β is the type of finite maps over a multiset. It is effectively a quotient of AList β by permutation of the underlying list.

Instances For
def AList.toFinmap {α : Type u} {β : αType v} (s : ) :

The quotient map from AList to Finmap.

Instances For
theorem AList.toFinmap_eq {α : Type u} {β : αType v} {s₁ : } {s₂ : } :
s₁.entries ~ s₂.entries
@[simp]
theorem AList.toFinmap_entries {α : Type u} {β : αType v} (s : ) :
().entries = s.entries
def List.toFinmap {α : Type u} {β : αType v} [] (s : List ()) :

Given l : List (Sigma β), create a term of type Finmap β by removing entries with duplicate keys.

Instances For
theorem Finmap.nodup_entries {α : Type u} {β : αType v} (f : ) :
Multiset.Nodup f.entries

### Lifting from AList #

def Finmap.liftOn {α : Type u} {β : αType v} {γ : Type u_1} (s : ) (f : γ) (H : ∀ (a b : ), a.entries ~ b.entriesf a = f b) :
γ

Lift a permutation-respecting function on AList to Finmap.

Instances For
@[simp]
theorem Finmap.liftOn_toFinmap {α : Type u} {β : αType v} {γ : Type u_1} (s : ) (f : γ) (H : ∀ (a b : ), a.entries ~ b.entriesf a = f b) :
= f s
def Finmap.liftOn₂ {α : Type u} {β : αType v} {γ : Type u_1} (s₁ : ) (s₂ : ) (f : γ) (H : ∀ (a₁ b₁ a₂ b₂ : ), a₁.entries ~ a₂.entriesb₁.entries ~ b₂.entriesf a₁ b₁ = f a₂ b₂) :
γ

Lift a permutation-respecting function on 2 ALists to 2 Finmaps.

Instances For
@[simp]
theorem Finmap.liftOn₂_toFinmap {α : Type u} {β : αType v} {γ : Type u_1} (s₁ : ) (s₂ : ) (f : γ) (H : ∀ (a₁ b₁ a₂ b₂ : ), a₁.entries ~ a₂.entriesb₁.entries ~ b₂.entriesf a₁ b₁ = f a₂ b₂) :
Finmap.liftOn₂ () () f H = f s₁ s₂

### Induction #

theorem Finmap.induction_on {α : Type u} {β : αType v} {C : Prop} (s : ) (H : (a : ) → C ()) :
C s
theorem Finmap.induction_on₂ {α : Type u} {β : αType v} {C : Prop} (s₁ : ) (s₂ : ) (H : (a₁ a₂ : ) → C () ()) :
C s₁ s₂
theorem Finmap.induction_on₃ {α : Type u} {β : αType v} {C : Prop} (s₁ : ) (s₂ : ) (s₃ : ) (H : (a₁ a₂ a₃ : ) → C () () ()) :
C s₁ s₂ s₃

### extensionality #

theorem Finmap.ext {α : Type u} {β : αType v} {s : } {t : } :
s.entries = t.entriess = t
@[simp]
theorem Finmap.ext_iff {α : Type u} {β : αType v} {s : } {t : } :
s.entries = t.entries s = t

### mem #

instance Finmap.instMembershipFinmap {α : Type u} {β : αType v} :

The predicate a ∈ s means that s has a value associated to the key a.

theorem Finmap.mem_def {α : Type u} {β : αType v} {a : α} {s : } :
a s a Multiset.keys s.entries
@[simp]
theorem Finmap.mem_toFinmap {α : Type u} {β : αType v} {a : α} {s : } :
a s

### keys #

def Finmap.keys {α : Type u} {β : αType v} (s : ) :

The set of keys of a finite map.

Instances For
@[simp]
theorem Finmap.keys_val {α : Type u} {β : αType v} (s : ) :
().val = ↑()
@[simp]
theorem Finmap.keys_ext {α : Type u} {β : αType v} {s₁ : } {s₂ : } :
~
theorem Finmap.mem_keys {α : Type u} {β : αType v} {a : α} {s : } :
a a s

### empty #

instance Finmap.instEmptyCollectionFinmap {α : Type u} {β : αType v} :

The empty map.

instance Finmap.instInhabitedFinmap {α : Type u} {β : αType v} :
@[simp]
theorem Finmap.empty_toFinmap {α : Type u} {β : αType v} :
@[simp]
theorem Finmap.toFinmap_nil {α : Type u} {β : αType v} [] :
theorem Finmap.not_mem_empty {α : Type u} {β : αType v} {a : α} :
@[simp]
theorem Finmap.keys_empty {α : Type u} {β : αType v} :

### singleton #

def Finmap.singleton {α : Type u} {β : αType v} (a : α) (b : β a) :

The singleton map.

Instances For
@[simp]
theorem Finmap.keys_singleton {α : Type u} {β : αType v} (a : α) (b : β a) :
= {a}
@[simp]
theorem Finmap.mem_singleton {α : Type u} {β : αType v} (x : α) (y : α) (b : β y) :
x x = y
instance Finmap.decidableEq {α : Type u} {β : αType v} [] [(a : α) → DecidableEq (β a)] :

### lookup #

def Finmap.lookup {α : Type u} {β : αType v} [] (a : α) (s : ) :
Option (β a)

Look up the value associated to a key in a map.

Instances For
@[simp]
theorem Finmap.lookup_toFinmap {α : Type u} {β : αType v} [] (a : α) (s : ) :
=
@[simp]
theorem Finmap.dlookup_list_toFinmap {α : Type u} {β : αType v} [] (a : α) (s : List ()) :
=
@[simp]
theorem Finmap.lookup_empty {α : Type u} {β : αType v} [] (a : α) :
= none
theorem Finmap.lookup_isSome {α : Type u} {β : αType v} [] {a : α} {s : } :
a s
theorem Finmap.lookup_eq_none {α : Type u} {β : αType v} [] {a : α} {s : } :
= none ¬a s
theorem Finmap.mem_lookup_iff {α : Type u} {β : αType v} [] {s : } {a : α} {b : β a} :
b { fst := a, snd := b } s.entries
theorem Finmap.lookup_eq_some_iff {α : Type u} {β : αType v} [] {s : } {a : α} {b : β a} :
= some b { fst := a, snd := b } s.entries
@[simp]
theorem Finmap.sigma_keys_lookup {α : Type u} {β : αType v} [] (s : ) :
(Finset.sigma () fun i => ) = { val := s.entries, nodup := (_ : Multiset.Nodup s.entries) }
@[simp]
theorem Finmap.lookup_singleton_eq {α : Type u} {β : αType v} [] {a : α} {b : β a} :
= some b
instance Finmap.instDecidableMemFinmapInstMembershipFinmap {α : Type u} {β : αType v} [] (a : α) (s : ) :
theorem Finmap.mem_iff {α : Type u} {β : αType v} [] {a : α} {s : } :
a s b, = some b
theorem Finmap.mem_of_lookup_eq_some {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } (h : = some b) :
a s
theorem Finmap.ext_lookup {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } :
(∀ (x : α), = ) → s₁ = s₂
@[simp]
theorem Finmap.keysLookupEquiv_apply_coe_fst {α : Type u} {β : αType v} [] (s : ) :
(↑(Finmap.keysLookupEquiv s)).fst =
@[simp]
theorem Finmap.keysLookupEquiv_apply_coe_snd {α : Type u} {β : αType v} [] (s : ) (i : α) :
Prod.snd (↑(Finmap.keysLookupEquiv s)) i =
def Finmap.keysLookupEquiv {α : Type u} {β : αType v} [] :
{ f // ∀ (i : α), Option.isSome (Prod.snd f i) = true i f.fst }

An equivalence between Finmap β and pairs (keys : Finset α, lookup : ∀ a, Option (β a)) such that (lookup a).isSome ↔ a ∈ keys.

Instances For
@[simp]
theorem Finmap.keysLookupEquiv_symm_apply_keys {α : Type u} {β : αType v} [] (f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true i f.fst }) :
Finmap.keys (Finmap.keysLookupEquiv.symm f) = (f).fst
@[simp]
theorem Finmap.keysLookupEquiv_symm_apply_lookup {α : Type u} {β : αType v} [] (f : { f // ∀ (i : α), Option.isSome (Prod.snd f i) = true i f.fst }) (a : α) :
Finmap.lookup a (Finmap.keysLookupEquiv.symm f) = Prod.snd (f) a

### replace #

def Finmap.replace {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :

Replace a key with a given value in a finite map. If the key is not present it does nothing.

Instances For
@[simp]
theorem Finmap.replace_toFinmap {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :
@[simp]
theorem Finmap.keys_replace {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :
@[simp]
theorem Finmap.mem_replace {α : Type u} {β : αType v} [] {a : α} {a' : α} {b : β a} {s : } :
a' a' s

### foldl #

def Finmap.foldl {α : Type u} {β : αType v} {δ : Type w} (f : δ(a : α) → β aδ) (H : ∀ (d : δ) (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂), f (f d a₁ b₁) a₂ b₂ = f (f d a₂ b₂) a₁ b₁) (d : δ) (m : ) :
δ

Fold a commutative function over the key-value pairs in the map

Instances For
def Finmap.any {α : Type u} {β : αType v} (f : (x : α) → β xBool) (s : ) :

any f s returns true iff there exists a value v in s such that f v = true.

Instances For
def Finmap.all {α : Type u} {β : αType v} (f : (x : α) → β xBool) (s : ) :

all f s returns true iff f v = true for all values v in s.

Instances For

### erase #

def Finmap.erase {α : Type u} {β : αType v} [] (a : α) (s : ) :

Erase a key from the map. If the key is not present it does nothing.

Instances For
@[simp]
theorem Finmap.erase_toFinmap {α : Type u} {β : αType v} [] (a : α) (s : ) :
=
@[simp]
theorem Finmap.keys_erase_toFinset {α : Type u} {β : αType v} [] (a : α) (s : ) :
@[simp]
theorem Finmap.keys_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
@[simp]
theorem Finmap.mem_erase {α : Type u} {β : αType v} [] {a : α} {a' : α} {s : } :
a' a' a a' s
theorem Finmap.not_mem_erase_self {α : Type u} {β : αType v} [] {a : α} {s : } :
@[simp]
theorem Finmap.lookup_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
Finmap.lookup a () = none
@[simp]
theorem Finmap.lookup_erase_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {s : } (h : a a') :
theorem Finmap.erase_erase {α : Type u} {β : αType v} [] {a : α} {a' : α} {s : } :

### sdiff #

def Finmap.sdiff {α : Type u} {β : αType v} [] (s : ) (s' : ) :

sdiff s s' consists of all key-value pairs from s and s' where the keys are in s or s' but not both.

Instances For
instance Finmap.instSDiffFinmap {α : Type u} {β : αType v} [] :

### insert #

def Finmap.insert {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :

Insert a key-value pair into a finite map, replacing any existing pair with the same key.

Instances For
@[simp]
theorem Finmap.insert_toFinmap {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :
theorem Finmap.insert_entries_of_neg {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } :
¬a s().entries = { fst := a, snd := b } ::ₘ s.entries
@[simp]
theorem Finmap.mem_insert {α : Type u} {β : αType v} [] {a : α} {a' : α} {b' : β a'} {s : } :
a Finmap.insert a' b' s a = a' a s
@[simp]
theorem Finmap.lookup_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} (s : ) :
@[simp]
theorem Finmap.lookup_insert_of_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {b : β a} (s : ) (h : a' a) :
@[simp]
theorem Finmap.insert_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} {b' : β a} (s : ) :
theorem Finmap.insert_insert_of_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {b : β a} {b' : β a'} (s : ) (h : a a') :
theorem Finmap.toFinmap_cons {α : Type u} {β : αType v} [] (a : α) (b : β a) (xs : List ()) :
List.toFinmap ({ fst := a, snd := b } :: xs) = Finmap.insert a b ()
theorem Finmap.mem_list_toFinmap {α : Type u} {β : αType v} [] (a : α) (xs : List ()) :
a b, { fst := a, snd := b } xs
@[simp]
theorem Finmap.insert_singleton_eq {α : Type u} {β : αType v} [] {a : α} {b : β a} {b' : β a} :

### extract #

def Finmap.extract {α : Type u} {β : αType v} [] (a : α) (s : ) :
Option (β a) ×

Erase a key from the map, and return the corresponding value, if found.

Instances For
@[simp]
theorem Finmap.extract_eq_lookup_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
= (, )

### union #

def Finmap.union {α : Type u} {β : αType v} [] (s₁ : ) (s₂ : ) :

s₁ ∪ s₂ is the key-based union of two finite maps. It is left-biased: if there exists an a ∈ s₁, lookup a (s₁ ∪ s₂) = lookup a s₁.

Instances For
instance Finmap.instUnionFinmap {α : Type u} {β : αType v} [] :
@[simp]
theorem Finmap.mem_union {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
a s₁ s₂ a s₁ a s₂
@[simp]
theorem Finmap.union_toFinmap {α : Type u} {β : αType v} [] (s₁ : ) (s₂ : ) :
= AList.toFinmap (s₁ s₂)
theorem Finmap.keys_union {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } :
Finmap.keys (s₁ s₂) =
@[simp]
theorem Finmap.lookup_union_left {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
a s₁Finmap.lookup a (s₁ s₂) =
@[simp]
theorem Finmap.lookup_union_right {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
¬a s₁Finmap.lookup a (s₁ s₂) =
theorem Finmap.lookup_union_left_of_not_in {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } (h : ¬a s₂) :
Finmap.lookup a (s₁ s₂) =
theorem Finmap.mem_lookup_union {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } :
b Finmap.lookup a (s₁ s₂) b ¬a s₁ b
theorem Finmap.mem_lookup_union_middle {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } {s₃ : } :
b Finmap.lookup a (s₁ s₃)¬a s₂b Finmap.lookup a (s₁ s₂ s₃)
theorem Finmap.insert_union {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } :
Finmap.insert a b (s₁ s₂) = Finmap.insert a b s₁ s₂
theorem Finmap.union_assoc {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } {s₃ : } :
s₁ s₂ s₃ = s₁ (s₂ s₃)
@[simp]
theorem Finmap.empty_union {α : Type u} {β : αType v} [] {s₁ : } :
s₁ = s₁
@[simp]
theorem Finmap.union_empty {α : Type u} {β : αType v} [] {s₁ : } :
s₁ = s₁
theorem Finmap.erase_union_singleton {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) (h : = some b) :
= s

### Disjoint #

def Finmap.Disjoint {α : Type u} {β : αType v} (s₁ : ) (s₂ : ) :

Disjoint s₁ s₂ holds if s₁ and s₂ have no keys in common.

Instances For
theorem Finmap.disjoint_empty {α : Type u} {β : αType v} (x : ) :
theorem Finmap.Disjoint.symm {α : Type u} {β : αType v} (x : ) (y : ) (h : ) :
theorem Finmap.Disjoint.symm_iff {α : Type u} {β : αType v} (x : ) (y : ) :
instance Finmap.instDecidableRelFinmapDisjoint {α : Type u} {β : αType v} [] :
DecidableRel Finmap.Disjoint
theorem Finmap.disjoint_union_left {α : Type u} {β : αType v} [] (x : ) (y : ) (z : ) :
theorem Finmap.disjoint_union_right {α : Type u} {β : αType v} [] (x : ) (y : ) (z : ) :
theorem Finmap.union_comm_of_disjoint {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } :
Finmap.Disjoint s₁ s₂s₁ s₂ = s₂ s₁
theorem Finmap.union_cancel {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } {s₃ : } (h : Finmap.Disjoint s₁ s₃) (h' : Finmap.Disjoint s₂ s₃) :
s₁ s₃ = s₂ s₃ s₁ = s₂