Documentation
FormalConjecturesForMathlib
.
Algebra
.
Group
.
Action
.
Pointwise
.
Set
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Imported by
Set
.
mul_mem_smul_set
Set
.
add_mem_vadd_set
source
@[simp]
theorem
Set
.
mul_mem_smul_set
{
M
:
Type
u_1}
[
Monoid
M
]
{
a
b
:
M
}
{
s
:
Set
M
}
[
IsLeftCancelMul
M
]
:
a
*
b
∈
a
•
s
↔
b
∈
s
source
@[simp]
theorem
Set
.
add_mem_vadd_set
{
M
:
Type
u_1}
[
AddMonoid
M
]
{
a
b
:
M
}
{
s
:
Set
M
}
[
IsLeftCancelAdd
M
]
:
a
+
b
∈
a
+ᵥ
s
↔
b
∈
s