mathlib3 documentation

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.

TODO #

Tags #

subsemigroup

theorem subsemigroup.mem_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_mul M] {S : ι subsemigroup M} (hS : directed has_le.le 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 : ι add_subsemigroup M} (hS : directed has_le.le 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 : ι add_subsemigroup M} (hS : directed has_le.le S) :
( (i : ι), S i) = (i : ι), (S i)
theorem subsemigroup.coe_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_mul M] {S : ι subsemigroup M} (hS : directed has_le.le 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 : directed_on has_le.le S) {x : M} :
x has_Sup.Sup S (s : subsemigroup M) (H : s S), x s
theorem add_subsemigroup.mem_Sup_of_directed_on {M : Type u_2} [has_add M] {S : set (add_subsemigroup M)} (hS : directed_on has_le.le S) {x : M} :
x has_Sup.Sup S (s : add_subsemigroup M) (H : s S), x 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 : ι subsemigroup M} (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 : ι add_subsemigroup M} (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} :
theorem add_subsemigroup.mem_Sup_of_mem {M : Type u_2} [has_add M] {S : set (add_subsemigroup M)} {s : add_subsemigroup M} (hs : s S) {x : M} :
theorem add_subsemigroup.supr_induction {ι : Sort u_1} {M : Type u_2} [has_add M] (S : ι add_subsemigroup M) {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 : ι subsemigroup M) {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 : ι subsemigroup M) {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 : ι add_subsemigroup M) {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.