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.

TODO #

Tags #

subsemigroup

abbrev AddSubsemigroup.mem_iSup_of_directed.match_1 {ι : Sort u_1} {M : Type u_2} [Add M] {S : ιAddSubsemigroup M} {x : M} (motive : (∃ (i : ι), x S i)Prop) :
∀ (x_1 : ∃ (i : ι), x S i), (∀ (i : ι) (hi : x S i), motive (_ : ∃ (i : ι), x S i))motive x_1
Equations
  • (_ : motive x) = (_ : motive x)
Instances For
    theorem AddSubsemigroup.mem_iSup_of_directed {ι : Sort u_1} {M : Type u_2} [Add M] {S : ιAddSubsemigroup M} (hS : Directed (fun (x x_1 : AddSubsemigroup M) => 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 : ιSubsemigroup M} (hS : Directed (fun (x x_1 : Subsemigroup M) => 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 : ιAddSubsemigroup M} (hS : Directed (fun (x x_1 : AddSubsemigroup M) => 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 : ιSubsemigroup M} (hS : Directed (fun (x x_1 : Subsemigroup M) => x x_1) S) :
    (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
    theorem AddSubsemigroup.mem_sSup_of_directed_on {M : Type u_2} [Add M] {S : Set (AddSubsemigroup M)} (hS : DirectedOn (fun (x x_1 : AddSubsemigroup M) => x x_1) S) {x : M} :
    x sSup S ∃ s ∈ S, x s
    theorem Subsemigroup.mem_sSup_of_directed_on {M : Type u_2} [Mul M] {S : Set (Subsemigroup M)} (hS : DirectedOn (fun (x x_1 : Subsemigroup M) => x x_1) S) {x : M} :
    x sSup S ∃ s ∈ S, x s
    theorem AddSubsemigroup.coe_sSup_of_directed_on {M : Type u_2} [Add M] {S : Set (AddSubsemigroup M)} (hS : DirectedOn (fun (x x_1 : AddSubsemigroup M) => x x_1) S) :
    (sSup S) = ⋃ s ∈ S, s
    theorem Subsemigroup.coe_sSup_of_directed_on {M : Type u_2} [Mul M] {S : Set (Subsemigroup M)} (hS : DirectedOn (fun (x x_1 : Subsemigroup M) => x x_1) S) :
    (sSup S) = ⋃ s ∈ S, s
    theorem AddSubsemigroup.mem_sup_left {M : Type u_2} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} {x : M} :
    x Sx S T
    theorem Subsemigroup.mem_sup_left {M : Type u_2} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} {x : M} :
    x Sx S T
    theorem AddSubsemigroup.mem_sup_right {M : Type u_2} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} {x : M} :
    x Tx S T
    theorem Subsemigroup.mem_sup_right {M : Type u_2} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} {x : M} :
    x Tx S T
    theorem AddSubsemigroup.add_mem_sup {M : Type u_2} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} {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 : Subsemigroup M} {T : Subsemigroup M} {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 : ιAddSubsemigroup M} (i : ι) {x : M} :
    x S ix iSup S
    theorem Subsemigroup.mem_iSup_of_mem {ι : Sort u_1} {M : Type u_2} [Mul M] {S : ιSubsemigroup M} (i : ι) {x : M} :
    x S ix iSup S
    theorem AddSubsemigroup.mem_sSup_of_mem {M : Type u_2} [Add M] {S : Set (AddSubsemigroup M)} {s : AddSubsemigroup M} (hs : s S) {x : M} :
    x sx sSup S
    theorem Subsemigroup.mem_sSup_of_mem {M : Type u_2} [Mul M] {S : Set (Subsemigroup M)} {s : Subsemigroup M} (hs : s S) {x : M} :
    x sx sSup S
    theorem AddSubsemigroup.iSup_induction {ι : Sort u_1} {M : Type u_2} [Add M] (S : ιAddSubsemigroup M) {C : MProp} {x₁ : M} (hx₁ : x₁ ⨆ (i : ι), S i) (hp : ∀ (i : ι), x₂S i, C 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 : ιSubsemigroup M) {C : MProp} {x₁ : M} (hx₁ : x₁ ⨆ (i : ι), S i) (hp : ∀ (i : ι), x₂S i, C 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 : ιAddSubsemigroup M) {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 : ιSubsemigroup M) {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.