# 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_iSup_of_directed, coe_iSup_of_directed, mem_sSup_of_directed_on, coe_sSup_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_iSup_of_directed.match_1 {ι : Sort u_1} {M : Type u_2} [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
Instances For
theorem AddSubsemigroup.mem_iSup_of_directed {ι : Sort u_1} {M : Type u_2} [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_iSup_of_directed {ι : Sort u_1} {M : Type u_2} [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_iSup_of_directed {ι : Sort u_1} {M : Type u_2} [Add M] {S : ι} (hS : Directed (fun x x_1 => x x_1) S) :
↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)
theorem Subsemigroup.coe_iSup_of_directed {ι : Sort u_1} {M : Type u_2} [Mul M] {S : ι} (hS : Directed (fun x x_1 => x x_1) S) :
↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)
theorem AddSubsemigroup.mem_sSup_of_directed_on {M : Type u_2} [Add M] {S : } (hS : DirectedOn (fun x x_1 => x x_1) S) {x : M} :
x sSup S s, s S x s
theorem Subsemigroup.mem_sSup_of_directed_on {M : Type u_2} [Mul M] {S : Set ()} (hS : DirectedOn (fun x x_1 => x x_1) S) {x : M} :
x sSup S s, s S x s
theorem AddSubsemigroup.coe_sSup_of_directed_on {M : Type u_2} [Add M] {S : } (hS : DirectedOn (fun x x_1 => x x_1) S) :
↑(sSup S) = ⋃ (s : ) (_ : s S), s
theorem Subsemigroup.coe_sSup_of_directed_on {M : Type u_2} [Mul M] {S : Set ()} (hS : DirectedOn (fun x x_1 => x x_1) S) :
↑(sSup S) = ⋃ (s : ) (_ : s S), s
theorem AddSubsemigroup.mem_sup_left {M : Type u_2} [Add M] {S : } {T : } {x : M} :
x Sx S T
theorem Subsemigroup.mem_sup_left {M : Type u_2} [Mul M] {S : } {T : } {x : M} :
x Sx S T
theorem AddSubsemigroup.mem_sup_right {M : Type u_2} [Add M] {S : } {T : } {x : M} :
x Tx S T
theorem Subsemigroup.mem_sup_right {M : Type u_2} [Mul M] {S : } {T : } {x : M} :
x Tx S T
theorem AddSubsemigroup.add_mem_sup {M : Type u_2} [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_2} [Mul M] {S : } {T : } {x : M} {y : M} (hx : x S) (hy : y T) :
x * y S T
theorem AddSubsemigroup.mem_iSup_of_mem {ι : Sort u_1} {M : Type u_2} [Add M] {S : ι} (i : ι) {x : M} :
x S ix iSup S
theorem Subsemigroup.mem_iSup_of_mem {ι : Sort u_1} {M : Type u_2} [Mul M] {S : ι} (i : ι) {x : M} :
x S ix iSup S
theorem AddSubsemigroup.mem_sSup_of_mem {M : Type u_2} [Add M] {S : } {s : } (hs : s S) {x : M} :
x sx sSup S
theorem Subsemigroup.mem_sSup_of_mem {M : Type u_2} [Mul M] {S : Set ()} {s : } (hs : s S) {x : M} :
x sx sSup S
theorem AddSubsemigroup.iSup_induction {ι : Sort u_1} {M : Type u_2} [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. 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.iSup_induction {ι : Sort u_1} {M : Type u_2} [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. 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.iSup_induction' {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι) {C : (x : M) → x ⨆ (i : ι), S iProp} (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.iSup_induction.

theorem Subsemigroup.iSup_induction' {ι : Sort u_1} {M : Type u_2} [Mul M] (S : ι) {C : (x : M) → x ⨆ (i : ι), S iProp} (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.iSup_induction.