Sym.ext
theorem Sym.ext : ∀ {α : Type u_1} {n : ℕ} {s₁ s₂ : Sym α n}, ↑s₁ = ↑s₂ → s₁ = s₂
The theorem `Sym.ext` asserts that for any type `α`, any natural number `n`, and any two symmetric powers `s₁` and `s₂` of `α` of order `n`, if the underlying multisets of `s₁` and `s₂` are equal (denoted by `↑s₁ = ↑s₂`), then `s₁` and `s₂` themselves must be equal. In other words, two n-tuples are considered identical in the nth symmetric power if they consist of the same elements, regardless of their order.
More concisely: In the n-th symmetric power of a type α, two multisets represent equal elements if and only if their corresponding symmetric powers are equal.
|
Sym.mem_cons_self
theorem Sym.mem_cons_self : ∀ {α : Type u_1} {n : ℕ} (a : α) (s : Sym α n), a ∈ a ::ₛ s
The theorem `Sym.mem_cons_self` states that for any type `α`, any natural number `n`, any element `a` of type `α`, and any `n`-tuple `s` (considered up to permutation) of type `α`, the element `a` is a member of the `n+1`-tuple created by prepending `a` to `s`. In other words, if you add an element to the start of a tuple, that element is definitely in the resulting tuple.
More concisely: For any type α, any natural number n, any element a of α, and any n-tuple s of type α considered up to permutation, the element a is in the (n+1)-tuple obtained by prepending a to s.
|
Sym.coe_injective
theorem Sym.coe_injective : ∀ {α : Type u_1} {n : ℕ}, Function.Injective Sym.toMultiset
The theorem `Sym.coe_injective` states that for any type `α` and any natural number `n`, the function `Sym.toMultiset` is injective. In other words, for any two elements of Sym of size `n`, if their mappings to `Multiset α` (derived via the function `Sym.toMultiset`) are the same, then the two original elements of Sym are also the same. This means that the `Sym.toMultiset` function does not map different Sym elements to the same Multiset, thereby preserving the uniqueness of Sym elements in the multiset representation.
More concisely: The `Sym.toMultiset` function maps distinct elements in `Sym` to distinct multisets.
|
Sym.map_id'
theorem Sym.map_id' : ∀ {α : Type u_3} {n : ℕ} (s : Sym α n), Sym.map (fun x => x) s = s
This theorem, `Sym.map_id'`, states that for any type `α` and any natural number `n`, if we have an element `s` of the type `Sym α n`, then applying the identity function to each element of the underlying `n`-tuple (which is performed by `Sym.map (fun x => x) s`) leaves `s` unchanged. In other words, mapping the identity function over any `Sym α n`-type element is an identity operation.
More concisely: For any type `α` and natural number `n`, the application of the identity function to each element of a permutation `s` of type `Sym α n` results in `s` itself: `Sym.map (fun x => x) s = s`.
|
Sym.map_map
theorem Sym.map_map :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {n : ℕ} (g : β → γ) (f : α → β) (s : Sym α n),
Sym.map g (Sym.map f s) = Sym.map (g ∘ f) s
This theorem states that for any types `α`, `β`, and `γ`, and for any natural number `n`, given two functions `g : β → γ` and `f : α → β`, and a n-tuple up to permutation `s` of type `Sym α n` (which is a subtype of `Multiset`), the process of first mapping `s` using `f` and then mapping the result using `g` is equivalent to directly mapping `s` using the composition of `g` and `f`. This property is called the functoriality of the symmetric powers. In mathematical terms, we could say that the map operations for symmetric powers are compatible with function composition, i.e., `Sym.map g (Sym.map f s) = Sym.map (g ∘ f) s`.
More concisely: For any types `α`, `β`, `γ`, natural number `n`, functions `g : β → γ` and `f : α → β`, and `n-tuple up to permutation s of type Sym α n`, the application of `g` to the image of `s` under `f` is equivalent to the composition of `g` and `f` applied to `s`, i.e., `Sym.map g (Sym.map f s) = Sym.map (g ∘ f) s`.
|
Sym.exists_mem
theorem Sym.exists_mem : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n.succ), ∃ a, a ∈ s
This theorem states that for any type `α` and any natural number `n`, if `s` is an `nth` symmetric power of `α` (which is a multiset of `α` with cardinally `n+1`), then there exists an element `a` that is a member of `s`. In other words, any such `nth` symmetric power `s` is non-empty.
More concisely: For any type `α` and natural number `n`, the `n`-th symmetric power of `α` is non-empty.
|
Sym.map_congr
theorem Sym.map_congr :
∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f g : α → β} {s : Sym α n},
(∀ x ∈ s, f x = g x) → Sym.map f s = Sym.map g s
The theorem `Sym.map_congr` states that for any types `α` and `β`, any natural number `n`, any functions `f` and `g` from `α` to `β`, and any symmetric `n`-tuple `s` of elements of type `α`, if `f` and `g` agree on all elements in `s`, then the result of mapping `f` over `s` using the function `Sym.map` is equal to the result of mapping `g` over `s`. In other words, if two functions agree on the elements of a symmetric `n`-tuple, they induce the same function on the symmetric power of the tuple.
More concisely: If functions $f$ and $g$ agree on components of a symmetric $n$-tuple $s$ in types $\alpha$ and $\beta$, then the application of the symmetric mapping `Sym.map` to $s$ with functions $f$ and $g$ results in equal outputs: $Sym.map(f)(s) = Sym.map(g)(s)$.
|
Sym.cons_erase
theorem Sym.cons_erase :
∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s), a ::ₛ s.erase a h = s := by
sorry
The theorem `Sym.cons_erase` states that for any type `α` with decidable equality, any `n`-th symmetric power `s` of `α` (which is a multiset of size `n+1`), and any element `a` of `α` that is in `s`, prepending `a` to the symmetric power obtained by erasing `a` from `s` yields the original symmetric power `s`. Essentially, it says that if you remove an element from a multiset and then prepend it again, you get back the original multiset.
More concisely: For any type `α` with decidable equality, for any natural number `n`, and for any `a` in an `n+1`-element symmetric power `s` of `α`, the operation of erasing `a` from `s` and then adding it back results in `s`. In mathematical notation, `(s \ a) ++ {a} = s`.
|