Mathlib.Algebra.Pointwise.Stabilizer._auxLemma.9
theorem Mathlib.Algebra.Pointwise.Stabilizer._auxLemma.9 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, (p = q) = ∀ (x : B), x ∈ p ↔ x ∈ q
This theorem, titled `_auxLemma.9` under the `Mathlib.Algebra.Pointwise.Stabilizer` namespace, states that for any two objects `p` and `q` of a type `A`, in a context where `A` behaves like a set of elements of another type `B`, the equality of `p` and `q` is equivalent to the condition that for every element `x` of type `B`, `x` is in `p` if and only if `x` is in `q`. Simply put, two objects are equal if and only if they contain exactly the same elements.
More concisely: For any objects $p$ and $q$ of a type $A$ behaving like a set in $B$, $p = q$ if and only if for all $x$ in $B$, $x$ is in $p$ if and only if $x$ is in $q$.
|
MulAction.stabilizer_coe_finset
theorem MulAction.stabilizer_coe_finset :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α] (s : Finset α),
MulAction.stabilizer G ↑s = MulAction.stabilizer G s
This theorem, `MulAction.stabilizer_coe_finset`, states that for any given finset `s` of a type `α` and a group `G` with a multiplicative action on `α`, if `α` has decidable equality, then the stabilizer of the co-domain of `s` under the group action is equal to the stabilizer of `s` itself under the same action. In other words, if `G` acts on `α` and `s` is a finite subset of `α`, the subgroup of elements in `G` that leave both `s` and its co-domain invariant under the action is the same. Here, `MulAction.stabilizer G a` is the subgroup of `G` that keeps an element `a` fixed under the action of `G`.
More concisely: For a finset `s` of type `α` and a multiplicative group `G` acting on `α` with decidable equality, the stabilizer of `s` and the stabilizer of its co-domain under `G` are equal.
|
Mathlib.Algebra.Pointwise.Stabilizer._auxAddLemma.10
theorem Mathlib.Algebra.Pointwise.Stabilizer._auxAddLemma.10 :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {a : G} {s : Set α},
(a ∈ AddAction.stabilizer G s) = ∀ (b : α), a +ᵥ b ∈ s ↔ b ∈ s
The given theorem, referred to as `Mathlib.Algebra.Pointwise.Stabilizer._auxAddLemma.10`, states that for any additive group `G` and any type `α` which has an additive action by `G`, and given an element `a` of `G` and a set `s` of elements of type `α`, `a` is in the stabilizer of `s` if and only if for every element `b` of type `α`, the result of the additive action of `a` on `b` (`a +ᵥ b`) is in `s` if and only if `b` is in `s`. In other words, `a` stabilizes `s` under the additive action `+ᵥ` if applying `a` to any element `b` of `s` results in another element of `s`, and conversely, if `b` is in `s`, then `a +ᵥ b` is also in `s`.
More concisely: An element `a` in an additive group `G` stabilizes a set `s` of elements in a type `α` under the additive action `+ᵥ` if and only if for all `b` in `s`, `a +ᵥ b` is also in `s`.
|
AddAction.stabilizer_coe_finset
theorem AddAction.stabilizer_coe_finset :
∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : DecidableEq α]
(s : Finset α), AddAction.stabilizer G ↑s = AddAction.stabilizer G s
This theorem states that for any given additive group `G`, any type `α`, and a finite set `s` of elements of type `α`, if `G` acts on `α` and `α` has decidable equality, then the stabilizer of the set `s` under this action is the same as the stabilizer of the coerced set `↑s`. In other words, the set of elements in `G` that leave `s` unchanged under the additive action is the same whether we consider `s` as a finite set or as a coerced set.
More concisely: For any additive group `G`, type `α` with decidable equality, and finite set `s` of `α`, if `G` acts on `α` and the stabilizer of `s` is defined, then the stabilizer of `s` equals the stabilizer of the coerced set `↑s`.
|
Mathlib.Algebra.Pointwise.Stabilizer._auxLemma.10
theorem Mathlib.Algebra.Pointwise.Stabilizer._auxLemma.10 :
∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α},
(a ∈ MulAction.stabilizer G s) = ∀ (b : α), a • b ∈ s ↔ b ∈ s
The theorem `Mathlib.Algebra.Pointwise.Stabilizer._auxLemma.10` states that, for any types `G` and `α`, with `G` a group and `α` a set on which `G` acts multiplicatively, for any element `a` of `G` and any set `s` of `α`, `a` belongs to the stabilizer of `s` under the action of `G` if and only if for every element `b` of `α`, `a` acting on `b` results in an element in `s` if and only if `b` is in `s`. In mathematical terms, this means that the stabilizing element `a` leaves every element in the set `s` invariant under the group action.
More concisely: For any group action of `G` on a set `α`, an element `a` in `G` stabilizes a set `s` if and only if for all `b` in `s`, `a` maps `b` to an element in `s`.
|
Mathlib.Algebra.Pointwise.Stabilizer._auxAddLemma.9
theorem Mathlib.Algebra.Pointwise.Stabilizer._auxAddLemma.9 :
∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, (p = q) = ∀ (x : B), x ∈ p ↔ x ∈ q
This theorem, named `Mathlib.Algebra.Pointwise.Stabilizer._auxAddLemma.9`, states that for any types `A` and `B`, with the condition that `A` is a subset-like structure of `B`, and for any elements `p` and `q` of type `A`, `p` is equal to `q` if and only if for all elements `x` of type `B`, `x` is in `p` exactly when `x` is in `q`. In other words, two elements of a subset-like structure are identical if they contain exactly the same elements.
More concisely: For any subset-like structures `A` of type `B` and elements `p` and `q` of type `A`, `p` equals `q` if and only if they contain the same elements of `B`.
|