Finmap.induction_on₂
theorem Finmap.induction_on₂ :
∀ {α : Type u} {β : α → Type v} {C : Finmap β → Finmap β → Prop} (s₁ s₂ : Finmap β),
(∀ (a₁ a₂ : AList β), C a₁.toFinmap a₂.toFinmap) → C s₁ s₂
This theorem states that, for any two finite maps `s₁` and `s₂` of type `Finmap β` indexed by an arbitrary type `α`, if a property `C` holds for any two associative lists `a₁` and `a₂` (of type `AList β`) when converted to `Finmap` using the function `AList.toFinmap`, then the same property `C` also holds for the finite maps `s₁` and `s₂`. Thus, the theorem provides an induction principle for establishing the equality of two finite maps based on their corresponding associative lists.
More concisely: If property `C` holds for any two associative lists when converted to finite maps, then property `C` holds for any two finite maps `s₁` and `s₂` of type `Finmap β` with corresponding associative lists `a₁` and `a₂`.
|
Finmap.erase_toFinmap
theorem Finmap.erase_toFinmap :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β),
Finmap.erase a s.toFinmap = (AList.erase a s).toFinmap
The theorem `Finmap.erase_toFinmap` states that for all types `α` and `β` (where `β` is a function of `α`), and for all `a` of type `α` and `s` of type `AList β`, if we have a function that can decide the equality of elements in `α`, then erasing `a` from the `Finmap` mapped from `AList` `s` is equivalent to first erasing `a` from `s` and then mapping the resulting `AList` to a `Finmap`. In other words, the operations of erasing an element and converting an `AList` to a `Finmap` can be performed in any order without affecting the outcome.
More concisely: For all types `α` and `β`, and for all `a : α` and `s : AList (β : α → Type)`, if `equiv` is a decidable equivalence relation on `α`, then erasing `a` from the `Finmap` obtained from `s` is equivalent to first erasing `a` from `s` and then mapping the resulting list to a `Finmap`.
|
Finmap.nodupKeys
theorem Finmap.nodupKeys : ∀ {α : Type u} {β : α → Type v} (self : Finmap β), self.entries.NodupKeys
This theorem states that for any typed finite map, represented by `Finmap β` where `β` is a function type mapping keys of type `α` to associated values, there are no duplicate keys in its entries. In other words, every key in this map is unique. The `entries` of the finite map are checked with `NodupKeys`, which asserts this property of having no duplicate keys.
More concisely: For any finite map `β` of type `Finmap α`, the keys `α` are pairwise distinct.
|
Finmap.keys.proof_1
theorem Finmap.keys.proof_1 : ∀ {α : Type u_1} {β : α → Type u_2} (s : Finmap β), s.entries.keys.Nodup
The theorem `Finmap.keys.proof_1` states that for every `Finmap`, which maps keys of any type `α` to elements of a type `β` defined by α, the multiset of keys extracted from its entries does not contain any duplicates. In other words, the multiset of keys, obtained by mapping each entry of the `Finmap` to its key, satisfies the property `Multiset.Nodup`, meaning that each key appears at most once.
More concisely: For every Finmap of type `α →β`, the multiset of keys (Image of the Finmap under the `Finmap.key` function) is a multiset of distinct elements.
|
AList.toFinmap_eq
theorem AList.toFinmap_eq :
∀ {α : Type u} {β : α → Type v} {s₁ s₂ : AList β}, s₁.toFinmap = s₂.toFinmap ↔ s₁.entries.Perm s₂.entries := by
sorry
The theorem `AList.toFinmap_eq` states that for any types `α` and `β : α → Type v`, and for any two `AList`s `s₁` and `s₂`, the `AList.toFinmap` of `s₁` is equal to the `AList.toFinmap` of `s₂` if and only if the entries of `s₁` are a permutation of the entries of `s₂`. In other words, two `AList`s have the same `Finmap` representation if and only if their entries can be rearranged to form each other.
More concisely: For any types `α` and `β : α → Type v`, the `AList.toFinmap` of two `AList`s of type `α` are equal if and only if their entries are permutations of each other.
|
Multiset.NodupKeys.nodup_keys
theorem Multiset.NodupKeys.nodup_keys :
∀ {α : Type u} {β : α → Type v} {m : Multiset ((a : α) × β a)}, m.NodupKeys → m.keys.Nodup
This theorem, known as an alias of the reverse direction of `Multiset.nodup_keys`, states that for any type `α`, a function `β` from `α` to some type `v`, and a multiset `m` of pairs consisting of an element of `α` and an element of `β a`, if the multiset `m` has no duplicate keys, then the keys of the multiset `m` are also without duplicates. This theorem assures that there are no repeat keys in the multiset, reinforcing the property of a multiset as a collection of elements where order does not matter but multiplicity does.
More concisely: If `m` is a multiset of pairs `(α × β)`, then the set `{a : α | ∃ (x, _) ∈ m.toList, x = a}` has no repeats.
|
Mathlib.Data.Finmap._auxLemma.16
theorem Mathlib.Data.Finmap._auxLemma.16 :
∀ {α : Type u} {β : α → Type v} {s₁ s₂ : AList β}, (s₁.toFinmap = s₂.toFinmap) = s₁.entries.Perm s₂.entries := by
sorry
This theorem, named `Mathlib.Data.Finmap._auxLemma.16`, states that for any two `AList` types `s₁` and `s₂` parameterized by types `α` and `β`, the condition for `s₁` being mapped to a `Finmap` type being equal to `s₂` being mapped to a `Finmap` type, is equivalent to the list of entries of `s₁` being a permutation of the list of entries of `s₂`. Here, `α` is any type and `β` is a type that depends on `α`. In other words, the theorem establishes a correspondence between equality of `Finmap` representations of two `ALists` and the permutation relation of their entries.
More concisely: For `AList` types `s₁` and `s₂` parameterized by types `α` and `β`, the `Finmap` representations of `s₁` and `s₂` are equal if and only if the lists of their entries are permutations of each other.
|
Finmap.union_toFinmap
theorem Finmap.union_toFinmap :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (s₁ s₂ : AList β),
s₁.toFinmap ∪ s₂.toFinmap = (s₁ ∪ s₂).toFinmap
This theorem states that for all types `α` and `β` (where `β` is a type dependent on `α`), and for all instances of decidable equality on `α`, and for all `s₁` and `s₂` which are association lists of type `β`, the union of the `Finmap` representations (i.e., finite maps), obtained from converting `s₁` and `s₂` using `AList.toFinmap`, is equal to the `Finmap` representation of the union of `s₁` and `s₂`. In other words, converting two association lists to finite maps and then taking their union is the same as first taking the union of the association lists and then converting to a finite map.
More concisely: For all types `α` and instances of decidable equality on `α`, the union of `Finmap.from AList` for two association lists `s₁` and `s₂` of type `β` (where `β` depends on `α`) is equal to `Finmap.union (Finmap.fromAList s₁) (Finmap.fromAList s₂)`.
|
Finmap.liftOn_toFinmap
theorem Finmap.liftOn_toFinmap :
∀ {α : Type u} {β : α → Type v} {γ : Type u_1} (s : AList β) (f : AList β → γ)
(H : ∀ (a b : AList β), a.entries.Perm b.entries → f a = f b), s.toFinmap.liftOn f H = f s
The theorem `Finmap.liftOn_toFinmap` states that for any AList `s`, function `f` from AList to some type `γ`, and a proof `H` that `f` respects permutations of the entries of ALists, the result of lifting `f` on the Finmap obtained from `s` by `AList.toFinmap` is the same as the result of applying `f` directly to `s`. In essence, it shows the consistency of `Finmap.liftOn` with `AList.toFinmap`, and thus allows us to work with well-defined functions on Finmaps derived from functions on ALists that respect permutations.
More concisely: For any permutation-respecting function `f` from an AList `s` to type `γ`, `Finmap.liftOn (AList.toFinmap s) f` is equal to `f s`.
|
Finmap.insert_toFinmap
theorem Finmap.insert_toFinmap :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : AList β),
Finmap.insert a b s.toFinmap = (AList.insert a b s).toFinmap
The theorem `Finmap.insert_toFinmap` states that for any types `α` and `β` such that `β` is a type function of `α`, and for any instance of decidable equality on `α`, any key `a` of type `α`, any value `b` of type `β a`, and any association list `s` of type `AList β`, the operation of inserting the key-value pair `(a, b)` into the finite map resulting from converting the association list `s` to a finite map is equivalent to the operation of converting the association list obtained from inserting the key-value pair `(a, b)` into `s` to a finite map. In other words, the process of inserting a key-value pair into an association list and then converting it to a finite map is the same as first converting the association list to a finite map and then inserting the key-value pair.
More concisely: For any type functions `β` of type `α`, and given a decidable equality on `α`, inserting a key-value pair `(a, b)` into the finite map constructed from an association list `s` is equivalent to constructing the finite map from the association list obtained by inserting `(a, b)` into `s`.
|
Finmap.induction_on
theorem Finmap.induction_on :
∀ {α : Type u} {β : α → Type v} {C : Finmap β → Prop} (s : Finmap β), (∀ (a : AList β), C a.toFinmap) → C s := by
sorry
The theorem `Finmap.induction_on` is a principle of induction for finite maps (`Finmap`). For every type `α`, a type `β` dependent on `α`, a property `C` about finite maps of `β`, and an instance `s` of a finite map of `β`, it states that if the property `C` holds for all finite maps that result from applying the function `AList.toFinmap` to any instance `a` of `AList β`, then the property `C` also holds for the finite map `s`.
More concisely: If `C` is a property that holds for all finite maps obtained by applying `AList.toFinmap` to any `AList β`, then `C` holds for the finite map `s` of type `Finmap β`.
|