Equiv.Perm.extendDomain_one
theorem Equiv.Perm.extendDomain_one :
∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
Equiv.Perm.extendDomain 1 f = 1
The theorem `Equiv.Perm.extendDomain_one` states that for any types `α` and `β`, a predicate `p` on `β`, and a decidable predicate instance on `p`, if we have an equivalence `f` between `α` and the subtype of `β` that satisfies `p`, then extending the domain of the identity permutation (denoted as `1`) using `f` results in the identity permutation. In other words, the process of extending the domain of the identity permutation using an equivalence does not change the permutation itself.
More concisely: Given types α and β, a predicate p on β with a decidable instance, and an equivalence f between α and the subtype of β satisfying p, the extension of the identity permutation on α using f remains the identity permutation.
|
Equiv.Perm.inv_apply_self
theorem Equiv.Perm.inv_apply_self : ∀ {α : Type u} (f : Equiv.Perm α) (x : α), f⁻¹ (f x) = x
The theorem `Equiv.Perm.inv_apply_self` states that for all types `α` and for all bijections `f` from `α` to itself (`f` is an element of `Equiv.Perm α`), applying `f⁻¹` (the inverse of `f`) to `f(x)` (the image of `x` under `f`) gives back `x`. In mathematical terms, this theorem is stating that for every bijection `f : α → α` and for all `x` in `α`, we have `f⁻¹(f(x)) = x`. This essentially captures the property that a bijection has an inverse such that applying the bijection followed by its inverse returns to the original element.
More concisely: For every bijection `f` from a type `α` to itself, `f⁻¹(f(x)) = x` for all `x` in `α`.
|
Equiv.Perm.ofSubtype_apply_of_not_mem
theorem Equiv.Perm.ofSubtype_apply_of_not_mem :
∀ {α : Type u} {p : α → Prop} [inst : DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)),
¬p a → (Equiv.Perm.ofSubtype f) a = a
This theorem states that for any type `α`, a predicate `p` on `α` that is decidable (i.e., for any element of `α` we can definitively say whether it satisfies `p` or not), a permutation `f` on the subtype of `α` determined by `p`, and an element `a` of `α` which does not satisfy `p` (i.e., `¬p a`), applying the permutation `f` extended to the whole type `α` to `a` results in `a` itself. In other words, the extension of `f` to `α` does not change elements that do not belong to the subtype defined by `p`.
More concisely: Let `α` be a type, `p` a decidable predicate on `α`, and `f` a permutation on the subtype `{x : α | p x}`. Then for all `a` not in `{x : α | p x}`, `f (a) = a`.
|
Equiv.Perm.permCongr_eq_mul
theorem Equiv.Perm.permCongr_eq_mul : ∀ {α : Type u} (e p : Equiv.Perm α), (Equiv.permCongr e) p = e * p * e⁻¹ := by
sorry
The theorem `Equiv.Perm.permCongr_eq_mul` expresses a property of permutations in the context of group theory. It states that for any type `α` and any permutations `e` and `p` over this type, applying the function `permCongr` with the permutation `e` to the permutation `p` is equivalent to multiplying `e` and `p` and then multiplying the result by the inverse of `e`. In mathematical terms, it's stating that `(permCongr e) p = e * p * e⁻¹` for all `e` and `p` that are permutations on the type `α`.
More concisely: For all types `α` and permutations `e` and `p` over `α`, `permCongr e p = e * p * e⁻¹`.
|
Equiv.Perm.inv_subtypePerm
theorem Equiv.Perm.inv_subtypePerm :
∀ {α : Type u} {p : α → Prop} (f : Equiv.Perm α) (hf : ∀ (x : α), p x ↔ p (f x)),
(f.subtypePerm hf)⁻¹ = f⁻¹.subtypePerm ⋯
The theorem `Equiv.Perm.inv_subtypePerm` states that for any type `α`, any property `p` on `α`, and any permutation (bijection) `f` on `α` that preserves the property `p` (meaning that `p` applies to `x` if and only if `p` applies to `f(x)`), the inverse of the restriction of `f` to the subtype of elements satisfying `p` is equal to the restriction to the same subtype of the inverse of `f`.
More concisely: If `f` is a permutation of type `α` that preserves the property `p`, then the restriction of `fⁱ` to the subtype of elements satisfying `p` is equal to the restriction of `f⁻¹` to that same subtype.
|
Equiv.Perm.mul_apply
theorem Equiv.Perm.mul_apply : ∀ {α : Type u} (f g : Equiv.Perm α) (x : α), (f * g) x = f (g x)
The theorem `Equiv.Perm.mul_apply` states that for any type `α`, and for any two permutations `f` and `g` of `α`, the function application of the product `(f * g)` at any element `x` of `α` is equal to the function application of `f` at the result of the function application of `g` at `x`. In other words, this theorem is explaining the composition of two permutations: applying the permutation `(f * g)` to `x` is the same as first applying the permutation `g` to `x` and then applying the permutation `f` to the result.
More concisely: For any type `α` and permutations `f` and `g` of `α`, `(f * g) x = f (g x)`.
|
Equiv.swap_inv
theorem Equiv.swap_inv : ∀ {α : Type u} [inst : DecidableEq α] (x y : α), (Equiv.swap x y)⁻¹ = Equiv.swap x y := by
sorry
The theorem `Equiv.swap_inv` states that for any type `α` with decidable equality and for any two elements `x` and `y` of this type, the inverse of the permutation that swaps `x` and `y` is the permutation that swaps `x` and `y` itself. This means that the operation of swapping two elements is its own inverse.
More concisely: For any type with decidable equality, the permutation that swaps two elements is equal to its own inverse.
|
Equiv.Perm.coe_pow
theorem Equiv.Perm.coe_pow : ∀ {α : Type u} (f : Equiv.Perm α) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
This theorem states that for any type `α`, a permutation `f` of type `α` and a natural number `n`, the application of the permutation `f` raised to the power of `n` (`f^n`) is equal to the `n`-fold iteration of the application of `f`. In mathematical terms, if `f` is a bijection from a set to itself, then applying `f^n` to an element is the same as applying `f` to that element `n` times.
More concisely: For any bijection (permutation) `f` and natural number `n`, `f^n` equals the `n`-fold composition of `f` with itself.
|
Set.BijOn.perm_inv
theorem Set.BijOn.perm_inv :
∀ {α : Type u_1} {f : Equiv.Perm α} {s : Set α}, Set.BijOn (⇑f) s s → Set.BijOn (⇑f⁻¹) s s
This theorem states that for any type `α`, given a permutation `f` (a bijective function) from `α` to `α` and a set `s` of type `α`, if `f` is bijective on the set `s` to itself (that is, `f` maps every element of `s` to a unique element in `s` and covers all elements of `s`), then the inverse of `f` is also bijective on the set `s` to itself. In other words, the inverse of a bijective function (permutation) on a set is again a bijective function on that same set.
More concisely: If `f` is a bijective function from a set `α` to itself, then the inverse function `f⁻¹` is also a bijective function from `f`'s image in `α` back to `α`.
|
Equiv.Perm.refl_mul
theorem Equiv.Perm.refl_mul : ∀ {α : Type u} (e : Equiv.Perm α), Equiv.refl α * e = e
The theorem `Equiv.Perm.refl_mul` states that for every type `α` and for every permutation `e` of `α` (i.e., a bijective function from `α` to itself), multiplying the identity function (represented as `Equiv.refl α`) with `e` results in `e`. In other words, the identity permutation acts as the multiplicative identity in the group of all permutations of a given type.
More concisely: For every type `α` and every permutation `e` of `α`, `Equiv.refl α * e = e`.
|
Equiv.Perm.inv_eq_iff_eq
theorem Equiv.Perm.inv_eq_iff_eq : ∀ {α : Type u} {f : Equiv.Perm α} {x y : α}, f⁻¹ x = y ↔ x = f y
This theorem states that for any given type `α`, for a permutation `f` of that type, and for any two elements `x` and `y` of that type, the image of `x` under the inverse of `f` being equal to `y` is equivalent to `x` being equal to the image of `y` under `f`. In other words, applying a permutation to an element and then applying the inverse permutation to the result returns the original element.
More concisely: For any permutation `f` of type `α` and elements `x, y : α`, `x = f⁻¹(y)` is equivalent to `y = f(x)`.
|
Equiv.swap_mul_involutive
theorem Equiv.swap_mul_involutive :
∀ {α : Type u} [inst : DecidableEq α] (i j : α), Function.Involutive fun x => Equiv.swap i j * x
This theorem, titled `Equiv.swap_mul_involutive`, states that for any given type `α` with a decidable equality, and any two elements `i` and `j` of that type, the operation of multiplying `x` by the permutation that swaps `i` and `j` is an involutive function. In other words, applying this operation twice to any `x` will return the original `x`. In mathematical terms, this can be written as `(swap i j * x) * (swap i j * x) = x` for all `x` in `α`. The term "involutive" here refers to the property of a function where its composition with itself yields the identity function.
More concisely: For any type `α` with decidable equality and any two elements `i` and `j` of `α`, the function that swaps `i` and `j` is an involutive operation on multiplication, i.e., `(swap i j * x) * (swap i j * x) = x` for all `x` in `α`.
|
Equiv.Perm.ofSubtype_apply_of_mem
theorem Equiv.Perm.ofSubtype_apply_of_mem :
∀ {α : Type u} {p : α → Prop} [inst : DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)) (ha : p a),
(Equiv.Perm.ofSubtype f) a = ↑(f ⟨a, ha⟩)
This theorem states that for any type `α` and a decidable predicate `p` on `α`, given a permutation `f` on the subtype of `α` satisfying `p`, and an element `a` of `α` that satisfies `p`, applying the permutation on `α` that extends `f` (obtained through `Equiv.Perm.ofSubtype`) to `a` yields the same result as applying `f` to `a` (considered as an element of the subtype). In other words, for those elements of `α` which satisfy `p`, the behavior of the extended permutation matches that of the original one.
More concisely: For any type `α` and decidable predicate `p` on `α`, if `f` is a permutation on the subtype of `α` satisfying `p`, then for all `a` in `α` satisfying `p`, `f a = (Equiv.Perm.ofSubtype f) a`.
|
Equiv.swap_mul_self_mul
theorem Equiv.swap_mul_self_mul :
∀ {α : Type u} [inst : DecidableEq α] (i j : α) (σ : Equiv.Perm α), Equiv.swap i j * (Equiv.swap i j * σ) = σ := by
sorry
The theorem `Equiv.swap_mul_self_mul` states that for any type `α` with decidable equality and any elements `i`, `j` of `α`, along with a permutation `σ` of `α`, the operation of left-multiplying the permutation `σ` with the swap function `swap i j` twice yields the original permutation `σ`. In other words, applying the swap operation twice, which swaps the positions of `i` and `j`, is equivalent to not making any changes to the permutation. This property is especially useful when working with cosets of permutations.
More concisely: For any permutation σ of type α with decidable equality, σ * swap i j * σ = swap i j.
|
Equiv.Perm.subtypePerm_inv
theorem Equiv.Perm.subtypePerm_inv :
∀ {α : Type u} {p : α → Prop} (f : Equiv.Perm α) (hf : ∀ (x : α), p x ↔ p (f⁻¹ x)),
f⁻¹.subtypePerm hf = (f.subtypePerm ⋯)⁻¹
The theorem `Equiv.Perm.subtypePerm_inv` states that for any type `α`, any predicate `p` over `α`, and any permutation `f` of `α` that preserves the predicate `p` (in the sense that `p x` holds if and only if `p (f⁻¹ x)` holds for all `x` in `α`), the inverse of the permutation restricted to the subtype determined by `p` (`f⁻¹.subtypePerm hf`) is equal to the inverse of the restriction of the permutation to the subtype determined by `p` (`(f.subtypePerm ⋯)⁻¹`).
More concisely: For any type α, predicate p over α, and permutation f preserving p, the inverse of f restricted to the subtype of α where p holds equals the inverse of the restriction of f to that subtype.
|
Equiv.mul_swap_involutive
theorem Equiv.mul_swap_involutive :
∀ {α : Type u} [inst : DecidableEq α] (i j : α), Function.Involutive fun x => x * Equiv.swap i j
The theorem `Equiv.mul_swap_involutive` asserts that for any type `α`, given a decidable equality on `α` and any two elements `i` and `j` from `α`, the operation of multiplying an element `x` from `α` by the permutation that swaps `i` and `j` (while leaving other values the same) is an involutive function. In other words, if you perform this operation twice on any element `x`, you will end up with `x` again. This can be interpreted as a stronger variant of the concept that multiplication by a certain element is injective.
More concisely: For any type `α` with decidable equality, the function that maps `x` to `x * (swap i j)` (where `swap i j` is the permutation swapping `i` and `j`), is an involutive function on `α`.
|
Equiv.Perm.extendDomain_mul
theorem Equiv.Perm.extendDomain_mul :
∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (e e' : Equiv.Perm α),
e.extendDomain f * e'.extendDomain f = (e * e').extendDomain f
The theorem `Equiv.Perm.extendDomain_mul` states that for all types `α` and `β`, and for a given predicate `p` on `β`, under a decidable condition on `p`, the operation `Equiv.Perm.extendDomain` on the product of two permutations `e` and `e'` of `α`, when applied with a bijection `f` from `α` to the subtype of `β` satisfying `p`, yields the same result as the product of the `Equiv.Perm.extendDomain` of `e` and `e'` individually applied with the same bijection `f`. In other words, the extension of the domain of the product of two permutations is the product of the extensions of the domains of the two permutations, when the permutations are bijective with a subset of another type.
More concisely: Given types `α`, `β`, a predicate `p` on `β` decidable under a condition, and bijective permutations `e` and `e'` of `α` with domains included in the subtype of `β` satisfying `p`, the extension of their product permutation equals the product of their individual extensions using the same bijection.
|
Equiv.Perm.apply_inv_self
theorem Equiv.Perm.apply_inv_self : ∀ {α : Type u} (f : Equiv.Perm α) (x : α), f (f⁻¹ x) = x
The theorem `Equiv.Perm.apply_inv_self` states that for any type `α`, any permutation (bijection) `f` from `α` to itself, and any element `x` of type `α`, applying `f` to the inverse of `x` under `f` gives `x` back. In other words, the inverse function undoes the effect of the function. This is essentially the property that characterizes bijections; they are invertible and applying a function followed by its inverse results in the original value.
More concisely: For any type `α` and bijection `f` from `α` to itself, `f (f⁻¹ x) = x` for all `x` in `α`.
|
Equiv.swap_mul_self
theorem Equiv.swap_mul_self : ∀ {α : Type u} [inst : DecidableEq α] (i j : α), Equiv.swap i j * Equiv.swap i j = 1 := by
sorry
The theorem `Equiv.swap_mul_self` states that for any type `α` that has decidable equality, and any two elements `i` and `j` of `α`, the permutation that swaps `i` and `j` twice is equal to the identity permutation. In other words, performing the swap operation twice will result in the original configuration, leaving all elements unchanged.
More concisely: For any type `α` with decidable equality, the swap permutation `i j => j i` is equal to the identity permutation on `α`.
|
Equiv.mul_swap_mul_self
theorem Equiv.mul_swap_mul_self :
∀ {α : Type u} [inst : DecidableEq α] (i j : α) (σ : Equiv.Perm α), σ * Equiv.swap i j * Equiv.swap i j = σ := by
sorry
The theorem `Equiv.mul_swap_mul_self` states that for any type `α` that has decidable equality, given two elements `i` and `j` of `α` and a permutation `σ` of `α`, right-multiplying the permutation `σ` by the permutation that swaps `i` and `j` twice, results in the original permutation `σ`. This property may be particularly useful when working with cosets of permutations. Essentially, it confirms that swapping the same elements twice in a permutation leaves the permutation unchanged.
More concisely: For any permutation σ of type α with decidable equality, σ * (swap i j * swap i j) = σ, where swap i j is the permutation that swaps i and j.
|