# Documentation

Mathlib.GroupTheory.Subsemigroup.Membership

# Subsemigroups: membership criteria #

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

• mem_supᵢ_of_directed, coe_supᵢ_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 FreeSemigroup 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 FreeSemigroup as the subsemigroup (pushed to be a semigroup) of the FreeMonoid consisting of non-identity elements.

## Tags #

subsemigroup

abbrev AddSubsemigroup.mem_supᵢ_of_directed.match_1 {ι : Sort u_1} {M : Type u_2} [inst : Add M] {S : ι} {x : M} (motive : (i, x S i) → Prop) :
(x : i, x S i) → ((i : ι) → (hi : x S i) → motive (_ : i, x S i)) → motive x
Equations
theorem AddSubsemigroup.mem_supᵢ_of_directed {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι} (hS : Directed (fun x x_1 => x x_1) S) {x : M} :
(x i, S i) i, x S i
theorem Subsemigroup.mem_supᵢ_of_directed {ι : Sort u_2} {M : Type u_1} [inst : Mul M] {S : ι} (hS : Directed (fun x x_1 => x x_1) S) {x : M} :
(x i, S i) i, x S i
theorem AddSubsemigroup.coe_supᵢ_of_directed {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι} (hS : Directed (fun x x_1 => x x_1) S) :
↑(i, S i) = Set.unionᵢ fun i => ↑(S i)
theorem Subsemigroup.coe_supᵢ_of_directed {ι : Sort u_2} {M : Type u_1} [inst : Mul M] {S : ι} (hS : Directed (fun x x_1 => x x_1) S) :
↑(i, S i) = Set.unionᵢ fun i => ↑(S i)
theorem AddSubsemigroup.mem_supₛ_of_directed_on {M : Type u_1} [inst : Add M] {S : } (hS : DirectedOn (fun x x_1 => x x_1) S) {x : M} :
x supₛ S s, s S x s
theorem Subsemigroup.mem_supₛ_of_directed_on {M : Type u_1} [inst : Mul M] {S : Set ()} (hS : DirectedOn (fun x x_1 => x x_1) S) {x : M} :
x supₛ S s, s S x s
theorem AddSubsemigroup.coe_supₛ_of_directed_on {M : Type u_1} [inst : Add M] {S : } (hS : DirectedOn (fun x x_1 => x x_1) S) :
↑(supₛ S) = Set.unionᵢ fun s => Set.unionᵢ fun h => s
theorem Subsemigroup.coe_supₛ_of_directed_on {M : Type u_1} [inst : Mul M] {S : Set ()} (hS : DirectedOn (fun x x_1 => x x_1) S) :
↑(supₛ S) = Set.unionᵢ fun s => Set.unionᵢ fun h => s
theorem AddSubsemigroup.mem_sup_left {M : Type u_1} [inst : Add M] {S : } {T : } {x : M} :
x Sx S T
theorem Subsemigroup.mem_sup_left {M : Type u_1} [inst : Mul M] {S : } {T : } {x : M} :
x Sx S T
theorem AddSubsemigroup.mem_sup_right {M : Type u_1} [inst : Add M] {S : } {T : } {x : M} :
x Tx S T
theorem Subsemigroup.mem_sup_right {M : Type u_1} [inst : Mul M] {S : } {T : } {x : M} :
x Tx S T
theorem AddSubsemigroup.add_mem_sup {M : Type u_1} [inst : Add M] {S : } {T : } {x : M} {y : M} (hx : x S) (hy : y T) :
x + y S T
theorem Subsemigroup.mul_mem_sup {M : Type u_1} [inst : Mul M] {S : } {T : } {x : M} {y : M} (hx : x S) (hy : y T) :
x * y S T
theorem AddSubsemigroup.mem_supᵢ_of_mem {ι : Sort u_2} {M : Type u_1} [inst : Add M] {S : ι} (i : ι) {x : M} :
x S ix supᵢ S
theorem Subsemigroup.mem_supᵢ_of_mem {ι : Sort u_2} {M : Type u_1} [inst : Mul M] {S : ι} (i : ι) {x : M} :
x S ix supᵢ S
theorem AddSubsemigroup.mem_supₛ_of_mem {M : Type u_1} [inst : Add M] {S : } {s : } (hs : s S) {x : M} :
x sx supₛ S
theorem Subsemigroup.mem_supₛ_of_mem {M : Type u_1} [inst : Mul M] {S : Set ()} {s : } (hs : s S) {x : M} :
x sx supₛ S
theorem AddSubsemigroup.supᵢ_induction {ι : Sort u_2} {M : Type u_1} [inst : Add M] (S : ι) {C : MProp} {x₁ : M} (hx₁ : x₁ i, S i) (hp : (i : ι) → (x₂ : M) → x₂ S iC x₂) (hmul : (x y : M) → C xC yC (x + y)) :
C x₁

An induction principle for elements of ⨆ i, S i⨆ 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.supᵢ_induction {ι : Sort u_2} {M : Type u_1} [inst : Mul M] (S : ι) {C : MProp} {x₁ : M} (hx₁ : x₁ i, S i) (hp : (i : ι) → (x₂ : M) → x₂ S iC x₂) (hmul : (x y : M) → C xC yC (x * y)) :
C x₁

An induction principle for elements of ⨆ i, S i⨆ 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 AddSubsemigroup.supᵢ_induction' {ι : Sort u_2} {M : Type u_1} [inst : Add M] (S : ι) {C : (x : M) → (x i, S i) → Prop} (hp : (i : ι) → (x : M) → (hxS : x S i) → C x (_ : x i, S i)) (hmul : (x y : M) → (hx : x i, S i) → (hy : y i, S i) → C x hxC y hyC (x + y) (_ : x + y i, S i)) {x₁ : M} (hx₁ : x₁ i, S i) :
C x₁ hx₁

A dependent version of AddSubsemigroup.supᵢ_induction.

theorem Subsemigroup.supᵢ_induction' {ι : Sort u_2} {M : Type u_1} [inst : Mul M] (S : ι) {C : (x : M) → (x i, S i) → Prop} (hp : (i : ι) → (x : M) → (hxS : x S i) → C x (_ : x i, S i)) (hmul : (x y : M) → (hx : x i, S i) → (hy : y i, S i) → C x hxC y hyC (x * y) (_ : x * y i, S i)) {x₁ : M} (hx₁ : x₁ i, S i) :
C x₁ hx₁

A dependent version of Subsemigroup.supᵢ_induction.