# mathlib3documentation

group_theory.subsemigroup.membership

# Subsemigroups: membership criteria #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove various facts about membership in a subsemigroup. The intent is to mimic group_theory/submonoid/membership, but currently this file is mostly a stub and only provides rudimentary support.

• mem_supr_of_directed, coe_supr_of_directed, mem_Sup_of_directed_on, coe_Sup_of_directed_on: the supremum of a directed collection of subsemigroup is their union.

## TODO #

• Define the free_semigroup generated by a set. This might require some rather substantial additions to low-level API. For example, developing the subtype of nonempty lists, then defining a product on nonempty lists, powers where the exponent is a positive natural, et cetera. Another option would be to define the free_semigroup as the subsemigroup (pushed to be a semigroup) of the free_monoid consisting of non-identity elements.

## Tags #

subsemigroup

theorem subsemigroup.mem_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_mul M] {S : ι } (hS : S) {x : M} :
(x (i : ι), S i) (i : ι), x S i
theorem add_subsemigroup.mem_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_add M] {S : ι } (hS : S) {x : M} :
(x (i : ι), S i) (i : ι), x S i
theorem add_subsemigroup.coe_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_add M] {S : ι } (hS : S) :
( (i : ι), S i) = (i : ι), (S i)
theorem subsemigroup.coe_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_mul M] {S : ι } (hS : S) :
( (i : ι), S i) = (i : ι), (S i)
theorem subsemigroup.mem_Sup_of_directed_on {M : Type u_2} [has_mul M] {S : set (subsemigroup M)} (hS : S) {x : M} :
x (s : (H : s S), x s
theorem add_subsemigroup.mem_Sup_of_directed_on {M : Type u_2} [has_add M] {S : set } (hS : S) {x : M} :
x (s : (H : s S), x s
theorem subsemigroup.coe_Sup_of_directed_on {M : Type u_2} [has_mul M] {S : set (subsemigroup M)} (hS : S) :
(has_Sup.Sup S) = (s : (H : s S), s
theorem add_subsemigroup.coe_Sup_of_directed_on {M : Type u_2} [has_add M] {S : set } (hS : S) :
(has_Sup.Sup S) = (s : (H : s S), s
theorem subsemigroup.mem_sup_left {M : Type u_2} [has_mul M] {S T : subsemigroup M} {x : M} :
x S x S T
theorem add_subsemigroup.mem_sup_left {M : Type u_2} [has_add M] {S T : add_subsemigroup M} {x : M} :
x S x S T
theorem add_subsemigroup.mem_sup_right {M : Type u_2} [has_add M] {S T : add_subsemigroup M} {x : M} :
x T x S T
theorem subsemigroup.mem_sup_right {M : Type u_2} [has_mul M] {S T : subsemigroup M} {x : M} :
x T x S T
theorem add_subsemigroup.add_mem_sup {M : Type u_2} [has_add M] {S T : add_subsemigroup M} {x y : M} (hx : x S) (hy : y T) :
x + y S T
theorem subsemigroup.mul_mem_sup {M : Type u_2} [has_mul M] {S T : subsemigroup M} {x y : M} (hx : x S) (hy : y T) :
x * y S T
theorem subsemigroup.mem_supr_of_mem {ι : Sort u_1} {M : Type u_2} [has_mul M] {S : ι } (i : ι) {x : M} :
x S i x supr S
theorem add_subsemigroup.mem_supr_of_mem {ι : Sort u_1} {M : Type u_2} [has_add M] {S : ι } (i : ι) {x : M} :
x S i x supr S
theorem subsemigroup.mem_Sup_of_mem {M : Type u_2} [has_mul M] {S : set (subsemigroup M)} {s : subsemigroup M} (hs : s S) {x : M} :
x s x
theorem add_subsemigroup.mem_Sup_of_mem {M : Type u_2} [has_add M] {S : set } {s : add_subsemigroup M} (hs : s S) {x : M} :
x s x
theorem add_subsemigroup.supr_induction {ι : Sort u_1} {M : Type u_2} [has_add M] (S : ι ) {C : M Prop} {x : M} (hx : x (i : ι), S i) (hp : (i : ι) (x : M), x S i C x) (hmul : (x y : M), C x C y C (x + y)) :
C x

An induction principle for elements of ⨆ i, S i. If C holds all elements of S i for all i, and is preserved under addition, then it holds for all elements of the supremum of S.

theorem subsemigroup.supr_induction {ι : Sort u_1} {M : Type u_2} [has_mul M] (S : ι ) {C : M Prop} {x : M} (hx : x (i : ι), S i) (hp : (i : ι) (x : M), x S i C x) (hmul : (x y : M), C x C y C (x * y)) :
C x

An induction principle for elements of ⨆ i, S i. If C holds all elements of S i for all i, and is preserved under multiplication, then it holds for all elements of the supremum of S.

theorem subsemigroup.supr_induction' {ι : Sort u_1} {M : Type u_2} [has_mul M] (S : ι ) {C : Π (x : M), (x (i : ι), S i) Prop} (hp : (i : ι) (x : M) (H : x S i), C x _) (hmul : (x y : M) (hx : x (i : ι), S i) (hy : y (i : ι), S i), C x hx C y hy C (x * y) _) {x : M} (hx : x (i : ι), S i) :
C x hx

A dependent version of subsemigroup.supr_induction.

theorem add_subsemigroup.supr_induction' {ι : Sort u_1} {M : Type u_2} [has_add M] (S : ι ) {C : Π (x : M), (x (i : ι), S i) Prop} (hp : (i : ι) (x : M) (H : x S i), C x _) (hmul : (x y : M) (hx : x (i : ι), S i) (hy : y (i : ι), S i), C x hx C y hy C (x + y) _) {x : M} (hx : x (i : ι), S i) :
C x hx

A dependent version of add_subsemigroup.supr_induction.