Subgroup.iSup_induction
theorem Subgroup.iSup_induction :
∀ {G : Type u_2} [inst : Group G] {ι : Sort u_5} (S : ι → Subgroup G) {C : G → Prop} {x : G},
x ∈ ⨆ i, S i → (∀ (i : ι), ∀ x ∈ S i, C x) → C 1 → (∀ (x y : G), C x → C y → C (x * y)) → C x
This theorem states an induction principle for elements of a supremum (denoted by `⨆ i, S i`) of subgroups in a group. Given a group `G`, an indexing type `ι`, a function `S` mapping each index to a subgroup, a property `C` over elements of `G`, and an element `x` of `G`, if `x` is an element of the supremum of `S`, `C` holds for `1` and all elements of each `S i`, and `C` is preserved under the multiplication operation (i.e., if `C` holds for `x` and `y`, then it holds for `x * y`), then `C` also holds for `x`.
More concisely: If `x` is an element of the supremum of subgroups `{S i | i ∈ ι}`, `C` holds for `1` and all elements of `S i`, and `C` is closed under multiplication, then `C` holds for `x`.
|
AddSubgroup.closure_induction_left
theorem AddSubgroup.closure_induction_left :
∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {p : (x : G) → x ∈ AddSubgroup.closure s → Prop},
p 0 ⋯ →
(∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (x + y) ⋯) →
(∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ AddSubgroup.closure s), p y hy → p (-x + y) ⋯) →
∀ {x : G} (h : x ∈ AddSubgroup.closure s), p x h
The theorem "AddSubgroup.closure_induction_left" states that for any type `G` equipped with an additive group structure, and any set `s` of elements of `G`, a property `p` holds for all elements in the additive subgroup generated by `s` if the property holds for the zero element and is preserved under addition and addition after negation with elements from `s` and the generated subgroup. Specifically, if `p` holds for `0`, and whenever `p` holds for an element `y` in the generated subgroup, `p` also holds for the sum of `y` with any element `x` from `s`, and the sum of the negation of `x` and `y`, then `p` holds for all elements in the generated subgroup. This is a form of induction tailored to the structure of an additive subgroup generated by a set of elements.
More concisely: If `p` is a property that holds for the zero element of an additive group `G` and is closed under addition and negation with elements from a set `s`, then `p` holds for all elements in the additive subgroup generated by `s`.
|
Subgroup.closure_induction_right
theorem Subgroup.closure_induction_right :
∀ {G : Type u_2} [inst : Group G] {s : Set G} {p : (x : G) → x ∈ Subgroup.closure s → Prop},
p 1 ⋯ →
(∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯) →
(∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯) →
∀ {x : G} (h : x ∈ Subgroup.closure s), p x h
The theorem `Subgroup.closure_induction_right` states that for any type `G` that forms a group, any set `s` of elements of `G`, and any property `p` that applies to elements of the closure of `s` under the subgroup operation, if the property holds for the identity element `1`, and if for any element `x` in the closure and any element `y` in the set `s`, the property being true of `x` implies that it's also true for the product `x * y` and the product `x * y⁻¹`, then the property holds for all elements of the closure of `s`. This is a kind of induction principle for properties of elements of the closure of a set under the subgroup operation.
More concisely: If `G` is a group, `s` is a subset of `G`, and `p` is a property that holds for the identity element and satisfies `p(x * y)` and `p(x * y⁻¹)` whenever `p(x)` holds for `x` in the closure of `s` and `y` in `s`, then `p` holds for all elements in the closure of `s`.
|
AddSubgroup.closure_induction''
theorem AddSubgroup.closure_induction'' :
∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {p : (g : G) → g ∈ AddSubgroup.closure s → Prop},
(∀ (x : G) (hx : x ∈ s), p x ⋯) →
(∀ (x : G) (hx : x ∈ s), p (-x) ⋯) →
p 0 ⋯ →
(∀ (x y : G) (hx : x ∈ AddSubgroup.closure s) (hy : y ∈ AddSubgroup.closure s),
p x hx → p y hy → p (x + y) ⋯) →
∀ {x : G} (h : x ∈ AddSubgroup.closure s), p x h
The theorem `AddSubgroup.closure_induction''` is an induction principle for membership in the additive closure of a set. It states that for any additive group `G`, set `s` of `G`, and property `p` defined on elements of the additive closure of `s`, if `p` holds for `0`, all elements of `s` and their negations, and if `p` is preserved under addition (i.e., if `x` and `y` satisfy `p` then so does `x + y`), then `p` holds for all elements of the additive closure of `s`.
More concisely: If a property `p` holds for 0, all elements of a set `s` and their negations, and is additively closed, then `p` holds for all elements in the additive closure of `s`.
|
AddSubgroup.iSup_induction'
theorem AddSubgroup.iSup_induction' :
∀ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_5} (S : ι → AddSubgroup G) {C : (x : G) → x ∈ ⨆ i, S i → Prop},
(∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯) →
C 0 ⋯ →
(∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯) →
∀ {x : G} (hx : x ∈ ⨆ i, S i), C x hx
This theorem is a dependent version of the `AddSubgroup.iSup_induction` theorem. It states that for all types `G` that form an additive group, and for a function `S` that assigns an additive subgroup of `G` to every element of a certain type `ι`, if a property `C` holds for all elements of each `S i`, the zero element, and the sum of any two elements of the union of `S i`, then `C` holds for every element of the union of `S i`.
More concisely: If `G` is an additive group, `S : ι → additive_subgroup G`, and for all `i: ι` and `x: S i`, `C x`, `C 0`, and `C (x + y)` hold for all `y: S i`, then `C x` holds for all `x: ⋃ i, S i`.
|
AddSubgroup.normal_add
theorem AddSubgroup.normal_add :
∀ {G : Type u_2} [inst : AddGroup G] (N H : AddSubgroup G) [inst_1 : N.Normal], ↑(N ⊔ H) = ↑N + ↑H
This theorem states that for any type `G` that is an additive group, given two additive subgroups `N` and `H` of `G`, if `N` is a normal subgroup, then the carrier of the join of `N` and `H` (denoted `N ⊔ H`) is equal to the pointwise set addition of `N` and `H` (denoted `↑N + ↑H`). In other words, each element in `N ⊔ H` is the sum of an element from `N` and an element from `H`.
More concisely: For any additive group `G`, if `N` is a normal subgroup of `G` and `N` and `H` are subgroups of `G`, then `N ⊔ H` equals the set of elements in `G` that can be written as the sum of an element from `N` and an element from `H`.
|
Subgroup.mul_normal
theorem Subgroup.mul_normal :
∀ {G : Type u_2} [inst : Group G] (H N : Subgroup G) [hN : N.Normal], ↑(H ⊔ N) = ↑H * ↑N
This theorem states that for any given group `G`, and any two of its subgroups `H` and `N`, where `N` is a normal subgroup, the carrier (i.e., the underlying set) of the join of `H` and `N` (`H ⊔ N`) is precisely the pointwise set product of the carriers of `H` and `N` (`↑H * ↑N`).
More concisely: For any group `G`, the carrier of `H ⊔ N`, where `H` is a subgroup and `N` is a normal subgroup, equals the set product of the carriers of `H` and `N`.
|
Subgroup.iSup_induction'
theorem Subgroup.iSup_induction' :
∀ {G : Type u_2} [inst : Group G] {ι : Sort u_5} (S : ι → Subgroup G) {C : (x : G) → x ∈ ⨆ i, S i → Prop},
(∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯) →
C 1 ⋯ →
(∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯) →
∀ {x : G} (hx : x ∈ ⨆ i, S i), C x hx
This theorem, `Subgroup.iSup_induction'`, is a dependent version of `Subgroup.iSup_induction`. It states that for any group `G` and any family of subgroups `S` indexed by `ι`, if a property `C` holds for every element in each subgroup `S i`, holds for the identity element `1` of the group, and is true for the product of any two elements `x` and `y` in the union of these subgroups `S i` provided `C` holds for `x` and `y`, then `C` is true for all elements in the union of the subgroups `S i`. This is a form of induction over an indexed family of subgroups of a group.
More concisely: Given a group `G` and a family `S` of subgroups indexed by `ι`, if `C` holds for the identity element `1` and for every pair of elements `x` and `y` in the union of the `S i` with `C` for `x` and `y`, then `C` holds for all elements in the union of the `S i`.
|
Subgroup.closure_induction''
theorem Subgroup.closure_induction'' :
∀ {G : Type u_2} [inst : Group G] {s : Set G} {p : (g : G) → g ∈ Subgroup.closure s → Prop},
(∀ (x : G) (hx : x ∈ s), p x ⋯) →
(∀ (x : G) (hx : x ∈ s), p x⁻¹ ⋯) →
p 1 ⋯ →
(∀ (x y : G) (hx : x ∈ Subgroup.closure s) (hy : y ∈ Subgroup.closure s), p x hx → p y hy → p (x * y) ⋯) →
∀ {x : G} (h : x ∈ Subgroup.closure s), p x h
This theorem provides an induction principle for proving properties about elements in a subgroup closure. In a given group `G`, for a set `s` and property `p`, if `p` holds for all elements of `s` and their inverses, `p` holds for the identity element `1`, and `p` is preserved under the group operation (i.e., if `p` holds for `x` and `y`, then `p` holds for `x * y`), then `p` holds for every element in the subgroup closure of `s`. This is essentially a way of saying that if a property is true for the generating set and preserved under the group operation, then it is true for the entire subgroup generated by the set.
More concisely: If a property holds for all elements and their inverses in a set `s` of a group `G`, for the identity element `1`, and is closed under group multiplication, then the property holds for every element in the subgroup generated by `s`.
|
AddSubgroup.closure_induction_right
theorem AddSubgroup.closure_induction_right :
∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {p : (x : G) → x ∈ AddSubgroup.closure s → Prop},
p 0 ⋯ →
(∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + y) ⋯) →
(∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + -y) ⋯) →
∀ {x : G} (h : x ∈ AddSubgroup.closure s), p x h
The theorem `AddSubgroup.closure_induction_right` asserts the following: for any type `G` that forms an additive group, a set `s` of elements of `G`, and a property `p` that applies to elements of the additive subgroup generated by `s`, if `p` holds for the additive identity `0`, and if `p` holds for any element `x` in the subgroup and any element `y` from the original set `s` when added to `x` or the additive inverse of `y` is added to `x` (given that `p` also holds for `x`), then `p` holds for all elements in the additive subgroup generated by `s`. This theorem allows us to use structural induction to prove properties of elements in additive subgroups generated by sets.
More concisely: Given an additive group G, a set s of its elements, and a property p that is closed under addition with elements in s and holds for the additive identity and elements x in the subgroup generated by s, then p holds for all elements in the subgroup generated by s.
|
Subgroup.closure_induction_left
theorem Subgroup.closure_induction_left :
∀ {G : Type u_2} [inst : Group G] {s : Set G} {p : (x : G) → x ∈ Subgroup.closure s → Prop},
p 1 ⋯ →
(∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x * y) ⋯) →
(∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x⁻¹ * y) ⋯) →
∀ {x : G} (h : x ∈ Subgroup.closure s), p x h
This theorem, `Subgroup.closure_induction_left`, is about induction on subgroups that are generated by a set of elements in a group. The theorem states that for any type `G` which forms a group, for any set `s` of elements of `G`, and for any property `p` pertaining to elements of `G` that are in the closure of the subgroup generated by `s`, if the property holds for the neutral element `1`, holds for any element `x` in `s` multiplied by any element `y` in the subgroup's closure provided `p` holds for `y`, and also holds for the inverse of any `x` in `s` multiplied by any `y` in the subgroup's closure provided `p` holds for `y`, then this property `p` holds for all elements `x` in the closure of the subgroup generated by `s`. This theorem allows us to apply induction principles to the closure of subgroups in the context of group theory.
More concisely: If `G` is a group, `s` is a set of elements in `G`, and `p` is a property that holds for the neutral element and for all `x` in `s` multiplied by any element `y` in the closure of the subgroup generated by `s` (respecting the inverse of `x`), then `p` holds for all elements in the closure of the subgroup generated by `s`.
|
AddSubgroup.iSup_induction
theorem AddSubgroup.iSup_induction :
∀ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_5} (S : ι → AddSubgroup G) {C : G → Prop} {x : G},
x ∈ ⨆ i, S i → (∀ (i : ι), ∀ x ∈ S i, C x) → C 0 → (∀ (x y : G), C x → C y → C (x + y)) → C x
This theorem, `AddSubgroup.iSup_induction`, states an induction principle for elements of the supremum of a family of additive subgroups `S` of an additive group `G`. Specifically, it says that if a property `C` holds for the zero element and for all elements of each `S i`, and if `C` is preserved under addition (i.e., if `C x` and `C y` both hold, then `C (x + y)` also holds), then `C` holds for all elements of the supremum of `S`.
More concisely: If `S` is a family of additive subgroups of an additive group `G`, and `C` is a property that holds for the zero element and is closed under addition, then `C` holds for the supremum of `S`.
|
AddSubgroup.add_normal
theorem AddSubgroup.add_normal :
∀ {G : Type u_2} [inst : AddGroup G] (H N : AddSubgroup G) [hN : N.Normal], ↑(H ⊔ N) = ↑H + ↑N
This theorem states that for any type `G` that is an additive group, given two additive subgroups `H` and `N` where `N` is a normal subgroup, the carrier of the join of `H` and `N` (`H ⊔ N`) is equal to the pointwise set addition of the carriers of `H` and `N` (`↑H + ↑N`). Here, `H ⊔ N` denotes the least subgroup containing both `H` and `N` and `↑H` and `↑N` denote the underlying sets of `H` and `N` respectively.
More concisely: For any additive group `G`, the carrier of `H ⊔ N`, the join of subgroups `H` and `N` with `N` being normal, equals the set-theoretic sum of the carriers of `H` and `N`: `↑(H ⊔ N) = ↑H + ↑N`.
|
Subgroup.normal_mul
theorem Subgroup.normal_mul :
∀ {G : Type u_2} [inst : Group G] (N H : Subgroup G) [inst_1 : N.Normal], ↑(N ⊔ H) = ↑N * ↑H
The theorem `Subgroup.normal_mul` states that for any group `G` and any two subgroups `N` and `H` of `G`, where `N` is a normal subgroup, the carrier of the join of `N` and `H` (denoted as `N ⊔ H`) is equal to the pointwise set product of the carriers of `N` and `H` (denoted as `↑N * ↑H`). In other words, every element in the union of the normal subgroup `N` and the subgroup `H` can be represented as a product of an element from `N` and an element from `H`.
More concisely: For any group `G`, if `N` is a normal subgroup of `G` and `H` is a subgroup of `G`, then `N ⊔ H` equals the set product `↑N * ↑H` of their carriers.
|