mathlib documentation

group_theory.subsemigroup.membership

Subsemigroups: membership criteria #

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.coe_Sup_of_directed_on {M : Type u_2} [has_mul M] {S : set (subsemigroup M)} (hS : directed_on has_le.le S) :
(has_Sup.Sup S) = ⋃ (s : subsemigroup M) (H : s S), s
theorem add_subsemigroup.coe_Sup_of_directed_on {M : Type u_2} [has_add M] {S : set (add_subsemigroup M)} (hS : directed_on has_le.le S) :
(has_Sup.Sup S) = ⋃ (s : add_subsemigroup M) (H : s S), s
theorem subsemigroup.mem_sup_left {M : Type u_2} [has_mul M] {S T : subsemigroup M} {x : M} :
x Sx S T
theorem add_subsemigroup.mem_sup_left {M : Type u_2} [has_add M] {S T : add_subsemigroup M} {x : M} :
x Sx S T
theorem add_subsemigroup.mem_sup_right {M : Type u_2} [has_add M] {S T : add_subsemigroup M} {x : M} :
x Tx S T
theorem subsemigroup.mem_sup_right {M : Type u_2} [has_mul M] {S T : subsemigroup M} {x : M} :
x Tx 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 ix 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 ix 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 sx has_Sup.Sup S
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} :
x sx has_Sup.Sup S
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 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.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 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 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 hxC y hyC (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 hxC y hyC (x + y) _) {x : M} (hx : x ⨆ (i : ι), S i) :
C x hx

A dependent version of add_subsemigroup.supr_induction.