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
FreeSemigroupgenerated 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 theFreeSemigroupas the subsemigroup (pushed to be a semigroup) of theFreeMonoidconsisting 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 : ι → AddSubsemigroup M}
{x : M}
(motive : (∃ i, x ∈ S i) → Prop)
:
Equations
- AddSubsemigroup.mem_supᵢ_of_directed.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h
theorem
AddSubsemigroup.coe_supᵢ_of_directed
{ι : Sort u_2}
{M : Type u_1}
[inst : Add M]
{S : ι → AddSubsemigroup M}
(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 : ι → Subsemigroup M}
(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 : Set (AddSubsemigroup M)}
(hS : DirectedOn (fun x x_1 => x ≤ x_1) S)
{x : M}
:
theorem
Subsemigroup.mem_supₛ_of_directed_on
{M : Type u_1}
[inst : Mul M]
{S : Set (Subsemigroup M)}
(hS : DirectedOn (fun x x_1 => x ≤ x_1) S)
{x : M}
:
theorem
AddSubsemigroup.coe_supₛ_of_directed_on
{M : Type u_1}
[inst : Add M]
{S : Set (AddSubsemigroup M)}
(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 (Subsemigroup M)}
(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 : AddSubsemigroup M}
{T : AddSubsemigroup M}
{x : M}
:
theorem
Subsemigroup.mem_sup_left
{M : Type u_1}
[inst : Mul M]
{S : Subsemigroup M}
{T : Subsemigroup M}
{x : M}
:
theorem
AddSubsemigroup.mem_sup_right
{M : Type u_1}
[inst : Add M]
{S : AddSubsemigroup M}
{T : AddSubsemigroup M}
{x : M}
:
theorem
Subsemigroup.mem_sup_right
{M : Type u_1}
[inst : Mul M]
{S : Subsemigroup M}
{T : Subsemigroup M}
{x : M}
:
theorem
AddSubsemigroup.add_mem_sup
{M : Type u_1}
[inst : Add M]
{S : AddSubsemigroup M}
{T : AddSubsemigroup M}
{x : M}
{y : M}
(hx : x ∈ S)
(hy : y ∈ T)
:
theorem
Subsemigroup.mul_mem_sup
{M : Type u_1}
[inst : Mul M]
{S : Subsemigroup M}
{T : Subsemigroup M}
{x : M}
{y : M}
(hx : x ∈ S)
(hy : y ∈ T)
:
theorem
AddSubsemigroup.mem_supᵢ_of_mem
{ι : Sort u_2}
{M : Type u_1}
[inst : Add M]
{S : ι → AddSubsemigroup M}
(i : ι)
{x : M}
:
theorem
Subsemigroup.mem_supᵢ_of_mem
{ι : Sort u_2}
{M : Type u_1}
[inst : Mul M]
{S : ι → Subsemigroup M}
(i : ι)
{x : M}
:
theorem
AddSubsemigroup.mem_supₛ_of_mem
{M : Type u_1}
[inst : Add M]
{S : Set (AddSubsemigroup M)}
{s : AddSubsemigroup M}
(hs : s ∈ S)
{x : M}
:
theorem
Subsemigroup.mem_supₛ_of_mem
{M : Type u_1}
[inst : Mul M]
{S : Set (Subsemigroup M)}
{s : Subsemigroup M}
(hs : s ∈ S)
{x : M}
:
theorem
AddSubsemigroup.supᵢ_induction
{ι : Sort u_2}
{M : Type u_1}
[inst : Add M]
(S : ι → AddSubsemigroup 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⨆ 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 : ι → 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⨆ 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 : ι → AddSubsemigroup M)
{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 hx → C y hy → C (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 : ι → Subsemigroup M)
{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 hx → C y hy → C (x * y) (_ : x * y ∈ ⨆ i, S i))
{x₁ : M}
(hx₁ : x₁ ∈ ⨆ i, S i)
:
C x₁ hx₁
A dependent version of Subsemigroup.supᵢ_induction.