Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self
theorem Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self :
∀ {α : Type u_1} {f : Equiv.Perm α} {x : α}, f x = x → ∀ (n : ℤ), (f ^ n) x = x
This theorem states that for any type `α`, given a permutation `f` (which is a bijection from `α` to itself), and an element `x` of `α`, if the permutation `f` applied to `x` gives `x` itself (i.e., `f` leaves `x` fixed), then for any integer `n`, the `n`-th iterated application of `f` (denoted by `f ^ n`) also leaves `x` fixed. In simpler terms, if a permutation does not change an element, repeated applications of this permutation won't change the element either, no matter how many times we apply it.
More concisely: If a permutation leaves an element fixed, then repeated applications of that permutation also leave that element fixed.
|
Equiv.Perm.pow_apply_eq_self_of_apply_eq_self
theorem Equiv.Perm.pow_apply_eq_self_of_apply_eq_self :
∀ {α : Type u_1} {f : Equiv.Perm α} {x : α}, f x = x → ∀ (n : ℕ), (f ^ n) x = x
The theorem `'Equiv.Perm.pow_apply_eq_self_of_apply_eq_self'` states that for any type `α`, any bijection `f` from `α` to itself (an element of `Equiv.Perm α`), and any element `x` of `α`, if `f` applied to `x` gives `x` (i.e., `f x = x`), then for any natural number `n`, applying `f` `n` times to `x` (i.e., `(f ^ n) x`) also gives `x`. In other words, if a permutation leaves an element unchanged, then repeated application of the permutation any number of times will also leave the element unchanged.
More concisely: If `f` is a bijection from a type `α` to itself and `f x = x` for some `x : α`, then `(f ^ n) x = x` for all natural numbers `n`.
|
Equiv.Perm.one_lt_card_support_of_ne_one
theorem Equiv.Perm.one_lt_card_support_of_ne_one :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f ≠ 1 → 1 < f.support.card := by
sorry
This theorem, `Equiv.Perm.one_lt_card_support_of_ne_one`, states that for any type `α` with decidable equality and finite number of elements, if a permutation `f` on `α` is not the identity permutation (represented by `1`), then the number of non-fixed points (`support`) of this permutation `f` is greater than one. Here, a non-fixed point of a permutation is an element that the permutation maps to a different element.
More concisely: For any finite type `α` with decidable equality, a non-identity permutation on `α` has at least 2 non-fixed points.
|
Equiv.Perm.Disjoint.symm
theorem Equiv.Perm.Disjoint.symm : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g → g.Disjoint f
The theorem `Equiv.Perm.Disjoint.symm` states that for any type `α` and any pair of permutations `f` and `g` over this type, if `f` and `g` are `Disjoint` (i.e., their supports are disjoint so that every element is either fixed by `f` or by `g`), then `g` and `f` are also `Disjoint`. This is a property of symmetry in the sense that the order of permutations in the `Disjoint` relation doesn't matter.
More concisely: For any type `α` and permutations `f` and `g` over it, if `f` and `g` are disjoint (i.e., their supports are disjoint), then `g` and `f` are also disjoint. (The symmetry property implies that the order of the permutations does not matter in the disjointness relation.)
|
Equiv.Perm.Disjoint.disjoint_support
theorem Equiv.Perm.Disjoint.disjoint_support :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
f.Disjoint g → Disjoint f.support g.support
The theorem `Equiv.Perm.Disjoint.disjoint_support` states that for any type `α` with decidable equality and finiteness, given two permutations `f` and `g` over `α`, if `f` and `g` are disjoint (i.e., for any element in `α`, it is either fixed by `f` or by `g`), then the sets of non-fixed points (or "supports") of `f` and `g` are also disjoint. Here, two sets are considered disjoint if their intersection is the empty set.
More concisely: Given permutations `f` and `g` over a finite type `α` with decidable equality, if `f` and `g` are disjoint, then their non-fixed point sets are disjoint.
|
Equiv.Perm.mem_support
theorem Equiv.Perm.mem_support :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α}, x ∈ f.support ↔ f x ≠ x
The theorem `Equiv.Perm.mem_support` states that for any type `α` with decidable equality and finite number of elements, and for any permutation `f` on `α` and any element `x` of `α`, the element `x` is in the support of the permutation `f` if and only if `f` of `x` is not equal to `x`. In other words, the support of a permutation is the set of all elements that are not fixed by the permutation.
More concisely: For any finite type `α` with decidable equality, a permutation `f` on `α` fixes an element `x` if and only if `x` is not in the support of `f`.
|
Equiv.Perm.not_mem_support
theorem Equiv.Perm.not_mem_support :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α}, x ∉ f.support ↔ f x = x
This theorem states that for any type `α` with decidable equality and finiteness, and any permutation `f` of this type and any element `x` of this type, `x` is not in the support of `f` if and only if `f` of `x` equals `x`. In other words, an element of a set is not in the set of nonfixed points of a permutation if and only if it is left unchanged by the permutation. This support set is determined by the function `f`, where the set consists of elements that do not remain the same after the function `f` is applied.
More concisely: For any permutation `f` on a type `α` with decidable equality and finite support, an element `x` of `α` is not in the support of `f` if and only if `f(x) = x`.
|
Equiv.Perm.support_one
theorem Equiv.Perm.support_one :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], Equiv.Perm.support 1 = ∅
The theorem `Equiv.Perm.support_one` states that for any type `α` which has decidable equality and is finite, the set of non-fixed points of the identity permutation (denoted as `1` in Lean) is empty. In other words, for any element of `α`, applying the identity permutation doesn't change the element, hence there are no non-fixed points.
More concisely: For any finite type `α` with decidable equality, the identity permutation fixes all elements, i.e., its non-fixed points are empty.
|
Equiv.Perm.apply_mem_support
theorem Equiv.Perm.apply_mem_support :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α},
f x ∈ f.support ↔ x ∈ f.support
This theorem, `Equiv.Perm.apply_mem_support`, states that for any type `α` with decidable equality and is a finite type, for any permutation `f` on `α`, and any `x` of type `α`, `x` is in the support of `f` if and only if the image of `x` under `f` is in the support of `f`.
In other words, it asserts that a point and its image under a permutation have the same status with regards to being a fixed point of the permutation: either both are fixed points, or neither is. The support of a permutation is the set of its non-fixed points.
More concisely: For any finite type `α` with decidable equality and permutation `f` on `α`, the element `x` is in the support of `f` if and only if `f(x)` is in the support of `f`.
|
Equiv.Perm.Disjoint.commute
theorem Equiv.Perm.Disjoint.commute : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g → Commute f g
The theorem `Equiv.Perm.Disjoint.commute` states that for any type `α` and any two permutations `f` and `g` of that type, if `f` and `g` are disjoint (meaning that for every element of `α`, it is left unchanged by either `f` or `g` but not both), then `f` and `g` commute. In other words, applying `f` and then `g` to any element of `α` yields the same result as applying `g` and then `f`.
More concisely: If two disjoint permutations on a type commute, then their order can be reversed without changing the result for any element of the type.
|
Mathlib.GroupTheory.Perm.Support._auxLemma.15
theorem Mathlib.GroupTheory.Perm.Support._auxLemma.15 :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α},
(x ∈ f.support) = (f x ≠ x)
This theorem, named `Mathlib.GroupTheory.Perm.Support._auxLemma.15`, states that for any type `α` with decidable equality and of finite size, for any permutation `f` on `α`, and for any element `x` of type `α`, `x` is in the support of the permutation `f` if and only if the permutation `f` does not fix `x`. In other words, the support of a permutation consists exactly of those elements which are not left unchanged by the permutation.
More concisely: For any finite type `α` with decidable equality, a permutation `f` on `α` fixes an element `x` if and only if `x` is not in the support of `f`.
|
Equiv.Perm.support_inv
theorem Equiv.Perm.support_inv :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (σ : Equiv.Perm α), σ⁻¹.support = σ.support
This theorem states that for any given type `α` with decidable equality and finite elements, and for any permutation `σ` of the type `α`, the set of non-fixed points of the inverse of `σ` is the same as the set of non-fixed points of `σ` itself. In other words, if we have a permutation `σ` that maps elements from `α` to other elements in `α`, the elements that don't remain in their original position when we apply `σ` are exactly the same elements that don't stay in their original position when we apply the inverse of `σ`. This is denoted by `Equiv.Perm.support σ⁻¹ = Equiv.Perm.support σ`.
More concisely: For any finite type `α` with decidable equality, the set of elements not fixed by a permutation `σ` is equal to the set of elements not fixed by its inverse.
|
Equiv.Perm.support_pow_le
theorem Equiv.Perm.support_pow_le :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (σ : Equiv.Perm α) (n : ℕ),
(σ ^ n).support ≤ σ.support
The theorem `Equiv.Perm.support_pow_le` states that for any type `α` with decidable equality and is finite, any permutation `σ` of `α`, and any natural number `n`, the set of non-fixed points of the `n`-th power of the permutation `σ` is a subset of the set of non-fixed points of the permutation `σ` itself. In other words, if a point is not moved by the `n`-th power of a permutation, it is also not moved by the original permutation.
More concisely: For any finite type `α` with decidable equality, any permutation `σ` of `α`, and natural number `n`, the set of elements not fixed by the `n`-th power of `σ` is a subset of the set of elements not fixed by `σ`.
|
Mathlib.GroupTheory.Perm.Support._auxLemma.16
theorem Mathlib.GroupTheory.Perm.Support._auxLemma.16 :
∀ {α : Type u_1} {s₁ s₂ : Finset α}, (s₁ = s₂) = ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂
This theorem, from the Group Theory and Permutation sections in the Mathlib library, states that for any type `α` and any two finite sets `s₁` and `s₂` of this type, `s₁` is equal to `s₂` if and only if for any element `a` of type `α`, `a` is in `s₁` if and only if `a` is in `s₂`. In other words, two finite sets are equal if they contain exactly the same elements.
More concisely: Two finite sets `s₁` and `s₂` of type `α` are equal if and only if they have the same elements.
|
Equiv.Perm.card_support_eq_zero
theorem Equiv.Perm.card_support_eq_zero :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f.support.card = 0 ↔ f = 1 := by
sorry
This theorem states that for any given type `α` that has decidable equality and is finite (i.e., has finiteness), and any given permutation `f` of `α`, the cardinality (i.e., the number of elements) of the set of non-fixed points of `f` is equal to zero if and only if `f` is the identity permutation. In other words, a permutation on a finite set with decidable equality has no non-fixed points (i.e., for every element `x`, `f(x) = x`) if and only if it is the identity permutation. This theorem links the structure of a permutation (i.e., whether it is the identity) with a property of its set of non-fixed points (i.e., whether this set is empty).
More concisely: A finite type with decidable equality has no non-fixed points under a permutation if and only if the permutation is the identity.
|
Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self
theorem Equiv.Perm.ne_and_ne_of_swap_mul_apply_ne_self :
∀ {α : Type u_1} [inst : DecidableEq α] {f : Equiv.Perm α} {x y : α},
(Equiv.swap x (f x) * f) y ≠ y → f y ≠ y ∧ y ≠ x
This theorem states that for any type `α` with decidable equality, any permutation `f` of `α`, and any elements `x` and `y` of `α`, if applying the permutation formed by first swapping `x` and `f x`, and then applying `f`, to `y` does not result in `y` (i.e., `(Equiv.swap x (f x) * f) y ≠ y`), then `f y` is not equal to `y` and `y` is not equal to `x` (i.e., `f y ≠ y ∧ y ≠ x`). In other words, if the combined swap and apply operation changes `y`, then the original permutation must also change `y`, and `y` can't be `x`.
More concisely: If `α` is a type with decidable equality, `f` is a permutation of `α`, `x` and `y` are elements of `α`, and `(Equiv.swap x (f x) * f) y = y` does not hold, then `f y ≠ y` and `y ≠ x`.
|
Equiv.Perm.disjoint_prod_right
theorem Equiv.Perm.disjoint_prod_right :
∀ {α : Type u_1} {f : Equiv.Perm α} (l : List (Equiv.Perm α)), (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod := by
sorry
The theorem `Equiv.Perm.disjoint_prod_right` states that for any type `α`, and any permutation `f` of this type, given a list `l` of such permutations, if `f` is disjoint with every permutation in the list `l` (meaning for every element, it is either fixed by `f` or by the permutation in `l`), then `f` is also disjoint with the product of all permutations in the list `l`. This product of permutations is computed as if applying each permutation in order, from right to left.
More concisely: If a permutation is disjoint with every permutation in a list, then it is disjoint with their right-to-left product.
|
Equiv.Perm.Disjoint.inv_left
theorem Equiv.Perm.Disjoint.inv_left : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g → f⁻¹.Disjoint g
The theorem `Equiv.Perm.Disjoint.inv_left` states that for any type `α` and any two permutations `f` and `g` on `α`, if `f` and `g` are disjoint (meaning their supports are disjoint, i.e., every element is fixed either by `f`, or by `g`), then the inverse of `f` and `g` are also disjoint. Here, the inverse of a permutation `f` is denoted as `f⁻¹`.
More concisely: If permutations `f` and `g` on type `α` have disjoint supports, then their inverses `f⁻¹` and `g⁻¹` also have disjoint supports.
|