Finite maps over Multiset

Multisets of sigma types

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

Multiset of keys of an association multiset.

Equations

• Multiset.keys s = Multiset.map Sigma.fst s

@[simp]

theorem Multiset.coe_keys {α : Type u} {β : α → Type v} {l : List (Sigma β)} : Multiset.keys ↑l = ↑(List.keys l)

def Multiset.NodupKeys {α : Type u} {β : α → Type v} (s : Multiset (Sigma β)) : Prop

NodupKeys s means that s has no duplicate keys.

Equations

• Multiset.NodupKeys s = Quot.liftOn s List.NodupKeys ⋯

@[simp]

theorem Multiset.coe_nodupKeys {α : Type u} {β : α → Type v} {l : List (Sigma β)} : Multiset.NodupKeys ↑l ↔ List.NodupKeys l

theorem Multiset.nodup_keys {α : Type u} {β : α → Type v} {m : Multiset ((a : α) × β a)} : Multiset.Nodup (Multiset.keys m) ↔ Multiset.NodupKeys m

theorem Multiset.NodupKeys.nodup_keys {α : Type u} {β : α → Type v} {m : Multiset ((a : α) × β a)} : Multiset.NodupKeys m → Multiset.Nodup (Multiset.keys m)

Alias of the reverse direction of Multiset.nodup_keys.

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

Finmap

structure Finmap {α : Type u} (β : α → Type v) : Type (max u v)

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

• entries : Multiset (Sigma β)

  The underlying Multiset of a Finmap

• nodupKeys : Multiset.NodupKeys self.entries

  There are no duplicate keys in entries

def AList.toFinmap {α : Type u} {β : α → Type v} (s : AList β) : Finmap β

The quotient map from AList to Finmap.

Equations

• AList.toFinmap s = { entries := ↑s.entries, nodupKeys := ⋯ }

theorem AList.toFinmap_eq {α : Type u} {β : α → Type v} {s₁ : AList β} {s₂ : AList β} : AList.toFinmap s₁ = AList.toFinmap s₂ ↔ List.Perm s₁.entries s₂.entries

@[simp]

theorem AList.toFinmap_entries {α : Type u} {β : α → Type v} (s : AList β) : (AList.toFinmap s).entries = ↑s.entries

def List.toFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (s : List (Sigma β)) : Finmap β

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

Equations

• List.toFinmap s = AList.toFinmap (List.toAList s)

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

Lifting from AList

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

Lift a permutation-respecting function on AList to Finmap.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finmap.liftOn_toFinmap {α : Type u} {β : α → Type v} {γ : Type u_1} (s : AList β) (f : AList β → γ) (H : ∀ (a b : AList β), List.Perm a.entries b.entries → f a = f b) : Finmap.liftOn (AList.toFinmap s) f H = f s

def Finmap.liftOn₂ {α : Type u} {β : α → Type v} {γ : Type u_1} (s₁ : Finmap β) (s₂ : Finmap β) (f : AList β → AList β → γ) (H : ∀ (a₁ b₁ a₂ b₂ : AList β), List.Perm a₁.entries a₂.entries → List.Perm b₁.entries b₂.entries → f a₁ b₁ = f a₂ b₂) : γ

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

Equations

• Finmap.liftOn₂ s₁ s₂ f H = Finmap.liftOn s₁ (fun (l₁ : AList β) => Finmap.liftOn s₂ (f l₁) ⋯) ⋯

@[simp]

theorem Finmap.liftOn₂_toFinmap {α : Type u} {β : α → Type v} {γ : Type u_1} (s₁ : AList β) (s₂ : AList β) (f : AList β → AList β → γ) (H : ∀ (a₁ b₁ a₂ b₂ : AList β), List.Perm a₁.entries a₂.entries → List.Perm b₁.entries b₂.entries → f a₁ b₁ = f a₂ b₂) : Finmap.liftOn₂ (AList.toFinmap s₁) (AList.toFinmap s₂) f H = f s₁ s₂

Induction

theorem Finmap.induction_on {α : Type u} {β : α → Type v} {C : Finmap β → Prop} (s : Finmap β) (H : ∀ (a : AList β), C (AList.toFinmap a)) : C s

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

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

extensionality

theorem Finmap.ext {α : Type u} {β : α → Type v} {s : Finmap β} {t : Finmap β} : s.entries = t.entries → s = t

@[simp]

theorem Finmap.ext_iff {α : Type u} {β : α → Type v} {s : Finmap β} {t : Finmap β} : s.entries = t.entries ↔ s = t

mem

instance Finmap.instMembershipFinmap {α : Type u} {β : α → Type v} : Membership α (Finmap β)

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

Equations

• Finmap.instMembershipFinmap = { mem := fun (a : α) (s : Finmap β) => a ∈ Multiset.keys s.entries }

theorem Finmap.mem_def {α : Type u} {β : α → Type v} {a : α} {s : Finmap β} : a ∈ s ↔ a ∈ Multiset.keys s.entries

@[simp]

theorem Finmap.mem_toFinmap {α : Type u} {β : α → Type v} {a : α} {s : AList β} : a ∈ AList.toFinmap s ↔ a ∈ s

keys

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

The set of keys of a finite map.

Equations

• Finmap.keys s = { val := Multiset.keys s.entries, nodup := ⋯ }

@[simp]

theorem Finmap.keys_val {α : Type u} {β : α → Type v} (s : AList β) : (Finmap.keys (AList.toFinmap s)).val = ↑(AList.keys s)

@[simp]

theorem Finmap.keys_ext {α : Type u} {β : α → Type v} {s₁ : AList β} {s₂ : AList β} : Finmap.keys (AList.toFinmap s₁) = Finmap.keys (AList.toFinmap s₂) ↔ List.Perm (AList.keys s₁) (AList.keys s₂)

theorem Finmap.mem_keys {α : Type u} {β : α → Type v} {a : α} {s : Finmap β} : a ∈ Finmap.keys s ↔ a ∈ s

empty

instance Finmap.instEmptyCollectionFinmap {α : Type u} {β : α → Type v} : EmptyCollection (Finmap β)

The empty map.

Equations

• Finmap.instEmptyCollectionFinmap = { emptyCollection := { entries := 0, nodupKeys := ⋯ } }

instance Finmap.instInhabitedFinmap {α : Type u} {β : α → Type v} : Inhabited (Finmap β)

Equations

• Finmap.instInhabitedFinmap = { default := ∅ }

@[simp]

theorem Finmap.empty_toFinmap {α : Type u} {β : α → Type v} : AList.toFinmap ∅ = ∅

@[simp]

theorem Finmap.toFinmap_nil {α : Type u} {β : α → Type v} [DecidableEq α] : List.toFinmap [] = ∅

theorem Finmap.not_mem_empty {α : Type u} {β : α → Type v} {a : α} : a ∉ ∅

@[simp]

theorem Finmap.keys_empty {α : Type u} {β : α → Type v} : Finmap.keys ∅ = ∅

singleton

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

The singleton map.

Equations

• Finmap.singleton a b = AList.toFinmap (AList.singleton a b)

@[simp]

theorem Finmap.keys_singleton {α : Type u} {β : α → Type v} (a : α) (b : β a) : Finmap.keys (Finmap.singleton a b) = {a}

@[simp]

theorem Finmap.mem_singleton {α : Type u} {β : α → Type v} (x : α) (y : α) (b : β y) : x ∈ Finmap.singleton y b ↔ x = y

instance Finmap.decidableEq {α : Type u} {β : α → Type v} [DecidableEq α] [(a : α) → DecidableEq (β a)] : DecidableEq (Finmap β)

Equations

• Finmap.decidableEq x✝ x = match x✝, x with | x, x_1 => decidable_of_iff (x.entries = x_1.entries) ⋯

lookup

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

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

Equations

• Finmap.lookup a s = Finmap.liftOn s (AList.lookup a) ⋯

@[simp]

theorem Finmap.lookup_toFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : Finmap.lookup a (AList.toFinmap s) = AList.lookup a s

@[simp]

theorem Finmap.dlookup_list_toFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : List (Sigma β)) : Finmap.lookup a (List.toFinmap s) = List.dlookup a s

@[simp]

theorem Finmap.lookup_empty {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) : Finmap.lookup a ∅ = none

theorem Finmap.lookup_isSome {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Finmap β} : Option.isSome (Finmap.lookup a s) = true ↔ a ∈ s

theorem Finmap.lookup_eq_none {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Finmap β} : Finmap.lookup a s = none ↔ a ∉ s

theorem Finmap.mem_lookup_iff {α : Type u} {β : α → Type v} [DecidableEq α] {s : Finmap β} {a : α} {b : β a} : b ∈ Finmap.lookup a s ↔ { fst := a, snd := b } ∈ s.entries

theorem Finmap.lookup_eq_some_iff {α : Type u} {β : α → Type v} [DecidableEq α] {s : Finmap β} {a : α} {b : β a} : Finmap.lookup a s = some b ↔ { fst := a, snd := b } ∈ s.entries

@[simp]

theorem Finmap.sigma_keys_lookup {α : Type u} {β : α → Type v} [DecidableEq α] (s : Finmap β) : (Finset.sigma (Finmap.keys s) fun (i : α) => Option.toFinset (Finmap.lookup i s)) = { val := s.entries, nodup := ⋯ }

@[simp]

theorem Finmap.lookup_singleton_eq {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} : Finmap.lookup a (Finmap.singleton a b) = some b

instance Finmap.instDecidableMemFinmapInstMembershipFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Decidable (a ∈ s)

Equations

• Finmap.instDecidableMemFinmapInstMembershipFinmap a s = decidable_of_iff (Option.isSome (Finmap.lookup a s) = true) ⋯

theorem Finmap.mem_iff {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Finmap β} : a ∈ s ↔ ∃ (b : β a), Finmap.lookup a s = some b

theorem Finmap.mem_of_lookup_eq_some {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} (h : Finmap.lookup a s = some b) : a ∈ s

theorem Finmap.ext_lookup {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} {s₂ : Finmap β} : (∀ (x : α), Finmap.lookup x s₁ = Finmap.lookup x s₂) → s₁ = s₂

@[simp]

theorem Finmap.keysLookupEquiv_apply_coe_fst {α : Type u} {β : α → Type v} [DecidableEq α] (s : Finmap β) : (↑(Finmap.keysLookupEquiv s)).1 = Finmap.keys s

@[simp]

theorem Finmap.keysLookupEquiv_apply_coe_snd {α : Type u} {β : α → Type v} [DecidableEq α] (s : Finmap β) (i : α) : (↑(Finmap.keysLookupEquiv s)).2 i = Finmap.lookup i s

def Finmap.keysLookupEquiv {α : Type u} {β : α → Type v} [DecidableEq α] : Finmap β ≃ { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), Option.isSome (f.2 i) = true ↔ i ∈ f.1 }

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finmap.keysLookupEquiv_symm_apply_keys {α : Type u} {β : α → Type v} [DecidableEq α] (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), Option.isSome (f.2 i) = true ↔ i ∈ f.1 }) : Finmap.keys (Finmap.keysLookupEquiv.symm f) = (↑f).1

@[simp]

theorem Finmap.keysLookupEquiv_symm_apply_lookup {α : Type u} {β : α → Type v} [DecidableEq α] (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), Option.isSome (f.2 i) = true ↔ i ∈ f.1 }) (a : α) : Finmap.lookup a (Finmap.keysLookupEquiv.symm f) = (↑f).2 a

replace

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

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

Equations

• Finmap.replace a b s = Finmap.liftOn s (fun (t : AList β) => AList.toFinmap (AList.replace a b t)) ⋯

@[simp]

theorem Finmap.replace_toFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : AList β) : Finmap.replace a b (AList.toFinmap s) = AList.toFinmap (AList.replace a b s)

@[simp]

theorem Finmap.keys_replace {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) : Finmap.keys (Finmap.replace a b s) = Finmap.keys s

@[simp]

theorem Finmap.mem_replace {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {b : β a} {s : Finmap β} : a' ∈ Finmap.replace a b s ↔ 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 : Finmap β) : δ

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

Equations

• Finmap.foldl f H d m = Multiset.foldl (fun (d : δ) (s : Sigma β) => f d s.fst s.snd) ⋯ d m.entries

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

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

Equations

• Finmap.any f s = Finmap.foldl (fun (x : Bool) (y : α) (z : β y) => x || f y z) ⋯ false s

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

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

Equations

• Finmap.all f s = Finmap.foldl (fun (x : Bool) (y : α) (z : β y) => x && f y z) ⋯ true s

erase

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

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

Equations

• Finmap.erase a s = Finmap.liftOn s (fun (t : AList β) => AList.toFinmap (AList.erase a t)) ⋯

@[simp]

theorem Finmap.erase_toFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : Finmap.erase a (AList.toFinmap s) = AList.toFinmap (AList.erase a s)

@[simp]

theorem Finmap.keys_erase_toFinset {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : Finmap.keys (AList.toFinmap (AList.erase a s)) = Finset.erase (Finmap.keys (AList.toFinmap s)) a

@[simp]

theorem Finmap.keys_erase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Finmap.keys (Finmap.erase a s) = Finset.erase (Finmap.keys s) a

@[simp]

theorem Finmap.mem_erase {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {s : Finmap β} : a' ∈ Finmap.erase a s ↔ a' ≠ a ∧ a' ∈ s

theorem Finmap.not_mem_erase_self {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Finmap β} : a ∉ Finmap.erase a s

@[simp]

theorem Finmap.lookup_erase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Finmap.lookup a (Finmap.erase a s) = none

@[simp]

theorem Finmap.lookup_erase_ne {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {s : Finmap β} (h : a ≠ a') : Finmap.lookup a (Finmap.erase a' s) = Finmap.lookup a s

theorem Finmap.erase_erase {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {s : Finmap β} : Finmap.erase a (Finmap.erase a' s) = Finmap.erase a' (Finmap.erase a s)

sdiff

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

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

Equations

• Finmap.sdiff s s' = Finmap.foldl (fun (s : Finmap β) (x : α) (x_1 : β x) => Finmap.erase x s) ⋯ s s'

instance Finmap.instSDiffFinmap {α : Type u} {β : α → Type v} [DecidableEq α] : SDiff (Finmap β)

Equations

• Finmap.instSDiffFinmap = { sdiff := Finmap.sdiff }

insert

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

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

Equations

• Finmap.insert a b s = Finmap.liftOn s (fun (t : AList β) => AList.toFinmap (AList.insert a b t)) ⋯

@[simp]

theorem Finmap.insert_toFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : AList β) : Finmap.insert a b (AList.toFinmap s) = AList.toFinmap (AList.insert a b s)

theorem Finmap.insert_entries_of_neg {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} : a ∉ s → (Finmap.insert a b s).entries = { fst := a, snd := b } ::ₘ s.entries

@[simp]

theorem Finmap.mem_insert {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {b' : β a'} {s : Finmap β} : a ∈ Finmap.insert a' b' s ↔ a = a' ∨ a ∈ s

@[simp]

theorem Finmap.lookup_insert {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} (s : Finmap β) : Finmap.lookup a (Finmap.insert a b s) = some b

@[simp]

theorem Finmap.lookup_insert_of_ne {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {b : β a} (s : Finmap β) (h : a' ≠ a) : Finmap.lookup a' (Finmap.insert a b s) = Finmap.lookup a' s

@[simp]

theorem Finmap.insert_insert {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {b' : β a} (s : Finmap β) : Finmap.insert a b' (Finmap.insert a b s) = Finmap.insert a b' s

theorem Finmap.insert_insert_of_ne {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {b : β a} {b' : β a'} (s : Finmap β) (h : a ≠ a') : Finmap.insert a' b' (Finmap.insert a b s) = Finmap.insert a b (Finmap.insert a' b' s)

theorem Finmap.toFinmap_cons {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (xs : List (Sigma β)) : List.toFinmap ({ fst := a, snd := b } :: xs) = Finmap.insert a b (List.toFinmap xs)

theorem Finmap.mem_list_toFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (xs : List (Sigma β)) : a ∈ List.toFinmap xs ↔ ∃ (b : β a), { fst := a, snd := b } ∈ xs

@[simp]

theorem Finmap.insert_singleton_eq {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {b' : β a} : Finmap.insert a b (Finmap.singleton a b') = Finmap.singleton a b

extract

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

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

Equations

• Finmap.extract a s = Finmap.liftOn s (fun (t : AList β) => Prod.map id AList.toFinmap (AList.extract a t)) ⋯

@[simp]

theorem Finmap.extract_eq_lookup_erase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : Finmap β) : Finmap.extract a s = (Finmap.lookup a s, Finmap.erase a s)

union

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

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₁.

Equations

• Finmap.union s₁ s₂ = Finmap.liftOn₂ s₁ s₂ (fun (s₁ s₂ : AList β) => AList.toFinmap (s₁ ∪ s₂)) ⋯

instance Finmap.instUnionFinmap {α : Type u} {β : α → Type v} [DecidableEq α] : Union (Finmap β)

Equations

• Finmap.instUnionFinmap = { union := Finmap.union }

@[simp]

theorem Finmap.mem_union {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ : Finmap β} {s₂ : Finmap β} : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂

@[simp]

theorem Finmap.union_toFinmap {α : Type u} {β : α → Type v} [DecidableEq α] (s₁ : AList β) (s₂ : AList β) : AList.toFinmap s₁ ∪ AList.toFinmap s₂ = AList.toFinmap (s₁ ∪ s₂)

theorem Finmap.keys_union {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} {s₂ : Finmap β} : Finmap.keys (s₁ ∪ s₂) = Finmap.keys s₁ ∪ Finmap.keys s₂

@[simp]

theorem Finmap.lookup_union_left {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ : Finmap β} {s₂ : Finmap β} : a ∈ s₁ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₁

@[simp]

theorem Finmap.lookup_union_right {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ : Finmap β} {s₂ : Finmap β} : a ∉ s₁ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₂

theorem Finmap.lookup_union_left_of_not_in {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ : Finmap β} {s₂ : Finmap β} (h : a ∉ s₂) : Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₁

theorem Finmap.mem_lookup_union {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ : Finmap β} {s₂ : Finmap β} : b ∈ Finmap.lookup a (s₁ ∪ s₂) ↔ b ∈ Finmap.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ Finmap.lookup a s₂

theorem Finmap.mem_lookup_union_middle {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ : Finmap β} {s₂ : Finmap β} {s₃ : Finmap β} : b ∈ Finmap.lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ Finmap.lookup a (s₁ ∪ s₂ ∪ s₃)

theorem Finmap.insert_union {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ : Finmap β} {s₂ : Finmap β} : Finmap.insert a b (s₁ ∪ s₂) = Finmap.insert a b s₁ ∪ s₂

theorem Finmap.union_assoc {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} {s₂ : Finmap β} {s₃ : Finmap β} : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

@[simp]

theorem Finmap.empty_union {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} : ∅ ∪ s₁ = s₁

@[simp]

theorem Finmap.union_empty {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} : s₁ ∪ ∅ = s₁

theorem Finmap.erase_union_singleton {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) (h : Finmap.lookup a s = some b) : Finmap.erase a s ∪ Finmap.singleton a b = s

Disjoint

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

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

Equations

• Finmap.Disjoint s₁ s₂ = ∀ x ∈ s₁, x ∉ s₂

theorem Finmap.disjoint_empty {α : Type u} {β : α → Type v} (x : Finmap β) : Finmap.Disjoint ∅ x

theorem Finmap.Disjoint.symm {α : Type u} {β : α → Type v} (x : Finmap β) (y : Finmap β) (h : Finmap.Disjoint x y) : Finmap.Disjoint y x

theorem Finmap.Disjoint.symm_iff {α : Type u} {β : α → Type v} (x : Finmap β) (y : Finmap β) : Finmap.Disjoint x y ↔ Finmap.Disjoint y x

instance Finmap.instDecidableRelFinmapDisjoint {α : Type u} {β : α → Type v} [DecidableEq α] : DecidableRel Finmap.Disjoint

Equations

• Finmap.instDecidableRelFinmapDisjoint x y = id inferInstance

theorem Finmap.disjoint_union_left {α : Type u} {β : α → Type v} [DecidableEq α] (x : Finmap β) (y : Finmap β) (z : Finmap β) : Finmap.Disjoint (x ∪ y) z ↔ Finmap.Disjoint x z ∧ Finmap.Disjoint y z

theorem Finmap.disjoint_union_right {α : Type u} {β : α → Type v} [DecidableEq α] (x : Finmap β) (y : Finmap β) (z : Finmap β) : Finmap.Disjoint x (y ∪ z) ↔ Finmap.Disjoint x y ∧ Finmap.Disjoint x z

theorem Finmap.union_comm_of_disjoint {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} {s₂ : Finmap β} : Finmap.Disjoint s₁ s₂ → s₁ ∪ s₂ = s₂ ∪ s₁

theorem Finmap.union_cancel {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : Finmap β} {s₂ : Finmap β} {s₃ : Finmap β} (h : Finmap.Disjoint s₁ s₃) (h' : Finmap.Disjoint s₂ s₃) : s₁ ∪ s₃ = s₂ ∪ s₃ ↔ s₁ = s₂