Documentation

Mathlib.Data.Finmap

Finite maps over Multiset #

Multisets of sigma types #

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

Multiset of keys of an association multiset.

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

    NodupKeys s means that s has no duplicate keys.

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

      Alias of the reverse direction of Multiset.nodup_keys.

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

      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.

      Instances For
        theorem Finmap.nodupKeys {α : Type u} {β : αType v} (self : Finmap β) :
        self.entries.NodupKeys

        There are no duplicate keys in entries

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

        The quotient map from AList to Finmap.

        Equations
        • s.toFinmap = { entries := s.entries, nodupKeys := }
        Instances For
          theorem AList.toFinmap_eq {α : Type u} {β : αType v} {s₁ : AList β} {s₂ : AList β} :
          s₁.toFinmap = s₂.toFinmap s₁.entries.Perm s₂.entries
          @[simp]
          theorem AList.toFinmap_entries {α : Type u} {β : αType v} (s : AList β) :
          s.toFinmap.entries = s.entries
          def List.toFinmap {α : Type u} {β : αType v} [DecidableEq α] (s : List (Sigma β)) :

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

          Equations
          • s.toFinmap = s.toAList.toFinmap
          Instances For
            theorem Finmap.nodup_entries {α : Type u} {β : αType v} (f : Finmap β) :
            f.entries.Nodup

            Lifting from AList #

            def Finmap.liftOn {α : Type u} {β : αType v} {γ : Type u_1} (s : Finmap β) (f : AList βγ) (H : ∀ (a b : AList β), a.entries.Perm b.entriesf 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.
            Instances For
              @[simp]
              theorem Finmap.liftOn_toFinmap {α : Type u} {β : αType v} {γ : Type u_1} (s : AList β) (f : AList βγ) (H : ∀ (a b : AList β), a.entries.Perm b.entriesf a = f b) :
              s.toFinmap.liftOn 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 β), a₁.entries.Perm a₂.entriesb₁.entries.Perm b₂.entriesf a₁ b₁ = f a₂ b₂) :
              γ

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

              Equations
              • s₁.liftOn₂ s₂ f H = s₁.liftOn (fun (l₁ : AList β) => s₂.liftOn (f l₁) )
              Instances For
                @[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 β), a₁.entries.Perm a₂.entriesb₁.entries.Perm b₂.entriesf a₁ b₁ = f a₂ b₂) :
                s₁.toFinmap.liftOn₂ s₂.toFinmap f H = f s₁ s₂

                Induction #

                theorem Finmap.induction_on {α : Type u} {β : αType v} {C : Finmap βProp} (s : Finmap β) (H : ∀ (a : AList β), C a.toFinmap) :
                C s
                theorem Finmap.induction_on₂ {α : Type u} {β : αType v} {C : Finmap βFinmap βProp} (s₁ : Finmap β) (s₂ : Finmap β) (H : ∀ (a₁ a₂ : AList β), C a₁.toFinmap a₂.toFinmap) :
                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 a₁.toFinmap a₂.toFinmap a₃.toFinmap) :
                C s₁ s₂ s₃

                extensionality #

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

                mem #

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

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

                Equations
                • Finmap.instMembership = { mem := fun (a : α) (s : Finmap β) => a s.entries.keys }
                theorem Finmap.mem_def {α : Type u} {β : αType v} {a : α} {s : Finmap β} :
                a s a s.entries.keys
                @[simp]
                theorem Finmap.mem_toFinmap {α : Type u} {β : αType v} {a : α} {s : AList β} :
                a s.toFinmap a s

                keys #

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

                The set of keys of a finite map.

                Equations
                • s.keys = { val := s.entries.keys, nodup := }
                Instances For
                  @[simp]
                  theorem Finmap.keys_val {α : Type u} {β : αType v} (s : AList β) :
                  s.toFinmap.keys.val = s.keys
                  @[simp]
                  theorem Finmap.keys_ext {α : Type u} {β : αType v} {s₁ : AList β} {s₂ : AList β} :
                  s₁.toFinmap.keys = s₂.toFinmap.keys s₁.keys.Perm s₂.keys
                  theorem Finmap.mem_keys {α : Type u} {β : αType v} {a : α} {s : Finmap β} :
                  a s.keys a s

                  empty #

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

                  The empty map.

                  Equations
                  • Finmap.instEmptyCollection = { emptyCollection := { entries := 0, nodupKeys := } }
                  instance Finmap.instInhabited {α : Type u} {β : αType v} :
                  Equations
                  • Finmap.instInhabited = { default := }
                  @[simp]
                  theorem Finmap.empty_toFinmap {α : Type u} {β : αType v} :
                  .toFinmap =
                  @[simp]
                  theorem Finmap.toFinmap_nil {α : Type u} {β : αType v} [DecidableEq α] :
                  [].toFinmap =
                  theorem Finmap.not_mem_empty {α : Type u} {β : αType v} {a : α} :
                  a
                  @[simp]
                  theorem Finmap.keys_empty {α : Type u} {β : αType v} :
                  .keys =

                  singleton #

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

                  The singleton map.

                  Equations
                  Instances For
                    @[simp]
                    theorem Finmap.keys_singleton {α : Type u} {β : αType v} (a : α) (b : β a) :
                    (Finmap.singleton a b).keys = {a}
                    @[simp]
                    theorem Finmap.mem_singleton {α : Type u} {β : αType v} (x : α) (y : α) (b : β y) :
                    instance Finmap.decidableEq {α : Type u} {β : αType v} [DecidableEq α] [(a : α) → DecidableEq (β a)] :
                    Equations
                    • x✝.decidableEq 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
                    Instances For
                      @[simp]
                      theorem Finmap.lookup_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
                      Finmap.lookup a s.toFinmap = AList.lookup a s
                      @[simp]
                      theorem Finmap.dlookup_list_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : List (Sigma β)) :
                      Finmap.lookup a s.toFinmap = List.dlookup a s
                      @[simp]
                      theorem Finmap.lookup_empty {α : Type u} {β : αType v} [DecidableEq α] (a : α) :
                      theorem Finmap.lookup_isSome {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Finmap β} :
                      (Finmap.lookup a s).isSome = true a s
                      theorem Finmap.lookup_eq_none {α : Type u} {β : αType v} [DecidableEq α] {a : α} {s : Finmap β} :
                      Finmap.lookup a s = none as
                      theorem Finmap.mem_lookup_iff {α : Type u} {β : αType v} [DecidableEq α] {s : Finmap β} {a : α} {b : β a} :
                      b Finmap.lookup a s a, 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 a, b s.entries
                      @[simp]
                      theorem Finmap.sigma_keys_lookup {α : Type u} {β : αType v} [DecidableEq α] (s : Finmap β) :
                      (s.keys.sigma fun (i : α) => (Finmap.lookup i s).toFinset) = { val := s.entries, nodup := }
                      @[simp]
                      theorem Finmap.lookup_singleton_eq {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} :
                      instance Finmap.instDecidableMem {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
                      Equations
                      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 = s.keys
                      @[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 : α), (f.2 i).isSome = 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.
                      Instances For
                        @[simp]
                        theorem Finmap.keysLookupEquiv_symm_apply_keys {α : Type u} {β : αType v} [DecidableEq α] (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true i f.1 }) :
                        (Finmap.keysLookupEquiv.symm f).keys = (f).1
                        @[simp]
                        theorem Finmap.keysLookupEquiv_symm_apply_lookup {α : Type u} {β : αType v} [DecidableEq α] (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = 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 β) :

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

                        Equations
                        Instances For
                          @[simp]
                          theorem Finmap.replace_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : AList β) :
                          Finmap.replace a b s.toFinmap = (AList.replace a b s).toFinmap
                          @[simp]
                          theorem Finmap.keys_replace {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : Finmap β) :
                          (Finmap.replace a b s).keys = s.keys
                          @[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
                          Instances For
                            def Finmap.any {α : Type u} {β : αType v} (f : (x : α) → β xBool) (s : Finmap β) :

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

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

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

                              Equations
                              Instances For

                                erase #

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

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

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Finmap.erase_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
                                  Finmap.erase a s.toFinmap = (AList.erase a s).toFinmap
                                  @[simp]
                                  theorem Finmap.keys_erase_toFinset {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : AList β) :
                                  (AList.erase a s).toFinmap.keys = s.toFinmap.keys.erase a
                                  @[simp]
                                  theorem Finmap.keys_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
                                  (Finmap.erase a s).keys = s.keys.erase 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 β} :
                                  aFinmap.erase a s
                                  @[simp]
                                  theorem Finmap.lookup_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :
                                  @[simp]
                                  theorem Finmap.lookup_erase_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {s : Finmap β} (h : a a') :
                                  theorem Finmap.erase_erase {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {s : Finmap β} :

                                  sdiff #

                                  def Finmap.sdiff {α : Type u} {β : αType v} [DecidableEq α] (s : Finmap β) (s' : 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
                                  Instances For
                                    instance Finmap.instSDiff {α : Type u} {β : αType v} [DecidableEq α] :
                                    Equations
                                    • Finmap.instSDiff = { sdiff := Finmap.sdiff }

                                    insert #

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

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

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Finmap.insert_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (s : AList β) :
                                      Finmap.insert a b s.toFinmap = (AList.insert a b s).toFinmap
                                      theorem Finmap.insert_entries_of_neg {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {s : Finmap β} :
                                      as(Finmap.insert a b s).entries = a, 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 β) :
                                      @[simp]
                                      theorem Finmap.lookup_insert_of_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {b : β a} (s : Finmap β) (h : a' a) :
                                      @[simp]
                                      theorem Finmap.insert_insert {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {b' : β a} (s : Finmap β) :
                                      theorem Finmap.insert_insert_of_ne {α : Type u} {β : αType v} [DecidableEq α] {a : α} {a' : α} {b : β a} {b' : β a'} (s : Finmap β) (h : a a') :
                                      theorem Finmap.toFinmap_cons {α : Type u} {β : αType v} [DecidableEq α] (a : α) (b : β a) (xs : List (Sigma β)) :
                                      (a, b :: xs).toFinmap = Finmap.insert a b xs.toFinmap
                                      theorem Finmap.mem_list_toFinmap {α : Type u} {β : αType v} [DecidableEq α] (a : α) (xs : List (Sigma β)) :
                                      a xs.toFinmap ∃ (b : β a), a, b xs
                                      @[simp]
                                      theorem Finmap.insert_singleton_eq {α : Type u} {β : αType v} [DecidableEq α] {a : α} {b : β a} {b' : β a} :

                                      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
                                      Instances For
                                        @[simp]
                                        theorem Finmap.extract_eq_lookup_erase {α : Type u} {β : αType v} [DecidableEq α] (a : α) (s : Finmap β) :

                                        union #

                                        def Finmap.union {α : Type u} {β : αType v} [DecidableEq α] (s₁ : Finmap β) (s₂ : 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
                                        • s₁.union s₂ = s₁.liftOn₂ s₂ (fun (s₁ s₂ : AList β) => (s₁ s₂).toFinmap)
                                        Instances For
                                          instance Finmap.instUnion {α : Type u} {β : αType v} [DecidableEq α] :
                                          Equations
                                          • Finmap.instUnion = { 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 β) :
                                          s₁.toFinmap s₂.toFinmap = (s₁ s₂).toFinmap
                                          theorem Finmap.keys_union {α : Type u} {β : αType v} [DecidableEq α] {s₁ : Finmap β} {s₂ : Finmap β} :
                                          (s₁ s₂).keys = s₁.keys s₂.keys
                                          @[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 β} :
                                          as₁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 : as₂) :
                                          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₁ as₁ 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₃)as₂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) :

                                          Disjoint #

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

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

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