# Pointwise action on sets #

This file proves that several kinds of actions of a type α on another type β transfer to actions of α/Set α on Set β.

## Implementation notes #

• We put all instances in the locale Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior of simp.

### Translation/scaling of sets #

theorem Set.op_vadd_set_subset_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} {a : α} :
a t s + t
theorem Set.op_smul_set_subset_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {a : α} :
a t s * t
theorem Set.image_op_vadd {α : Type u_2} [Add α] {s : Set α} {t : Set α} :
AddOpposite.op '' s +ᵥ t = t + s
theorem Set.image_op_smul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} :
MulOpposite.op '' s t = t * s
@[simp]
theorem Set.iUnion_op_vadd_set {α : Type u_2} [Add α] (s : Set α) (t : Set α) :
at, = s + t
@[simp]
theorem Set.iUnion_op_smul_set {α : Type u_2} [Mul α] (s : Set α) (t : Set α) :
at, = s * t
theorem Set.add_subset_iff_left {α : Type u_2} [Add α] {s : Set α} {t : Set α} {u : Set α} :
s + t u as, a +ᵥ t u
theorem Set.mul_subset_iff_left {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {u : Set α} :
s * t u as, a t u
theorem Set.add_subset_iff_right {α : Type u_2} [Add α] {s : Set α} {t : Set α} {u : Set α} :
s + t u bt, u
theorem Set.mul_subset_iff_right {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {u : Set α} :
s * t u bt, u
theorem Set.range_add {α : Type u_2} [Add α] {ι : Sort u_5} (a : α) (f : ια) :
(Set.range fun (i : ι) => a + f i) = a +ᵥ
theorem Set.range_mul {α : Type u_2} [Mul α] {ι : Sort u_5} (a : α) (f : ια) :
(Set.range fun (i : ι) => a * f i) = a
instance Set.vaddCommClass_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Set.smulCommClass_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [] :
SMulCommClass α β (Set γ)
Equations
• =
instance Set.vaddCommClass_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [] :
VAddCommClass α (Set β) (Set γ)
Equations
• =
instance Set.smulCommClass_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [] :
SMulCommClass α (Set β) (Set γ)
Equations
• =
instance Set.vaddCommClass_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [] :
VAddCommClass (Set α) β (Set γ)
Equations
• =
instance Set.smulCommClass_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [] :
SMulCommClass (Set α) β (Set γ)
Equations
• =
instance Set.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [] :
VAddCommClass (Set α) (Set β) (Set γ)
Equations
• =
instance Set.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [] :
SMulCommClass (Set α) (Set β) (Set γ)
Equations
• =
instance Set.vaddAssocClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [] :
Equations
• =
instance Set.isScalarTower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [] :
IsScalarTower α β (Set γ)
Equations
• =
instance Set.vaddAssocClass' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [] :
VAddAssocClass α (Set β) (Set γ)
Equations
• =
instance Set.isScalarTower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [] :
IsScalarTower α (Set β) (Set γ)
Equations
• =
instance Set.vaddAssocClass'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [VAdd α γ] [VAdd β γ] [] :
VAddAssocClass (Set α) (Set β) (Set γ)
Equations
• =
instance Set.isScalarTower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [] :
IsScalarTower (Set α) (Set β) (Set γ)
Equations
• =
instance Set.isCentralVAdd {α : Type u_2} {β : Type u_3} [VAdd α β] [VAdd αᵃᵒᵖ β] [] :
Equations
• =
instance Set.isCentralScalar {α : Type u_2} {β : Type u_3} [SMul α β] [SMul αᵐᵒᵖ β] [] :
Equations
• =
theorem Set.addAction.proof_2 {α : Type u_1} {β : Type u_2} [] [] :
∀ (x x_1 : Set α) (x_2 : Set β), Set.image2 (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) (Set.image2 (fun (x1 x2 : α) => x1 + x2) x x_1) x_2 = Set.image2 (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) x (Set.image2 (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) x_1 x_2)
def Set.addAction {α : Type u_2} {β : Type u_3} [] [] :

An additive action of an additive monoid α on a type β gives an additive action of Set α on Set β

Equations
Instances For
theorem Set.addAction.proof_1 {α : Type u_2} {β : Type u_1} [] [] (s : Set β) :
Set.image2 (fun (x1 : α) (x2 : β) => x1 +ᵥ x2) {0} s = s
def Set.mulAction {α : Type u_2} {β : Type u_3} [] [] :
MulAction (Set α) (Set β)

A multiplicative action of a monoid α on a type β gives a multiplicative action of Set α on Set β.

Equations
• Set.mulAction =
Instances For
theorem Set.addActionSet.proof_2 {α : Type u_2} {β : Type u_1} [] [] :
∀ (x x_1 : α) (x_2 : Set β), (fun (x_3 : β) => x + x_1 +ᵥ x_3) '' x_2 = (fun (x_3 : β) => x +ᵥ x_3) '' ((fun (x : β) => x_1 +ᵥ x) '' x_2)
theorem Set.addActionSet.proof_1 {α : Type u_2} {β : Type u_1} [] [] :
∀ (x : Set β), (fun (x : β) => 0 +ᵥ x) '' x = x
def Set.addActionSet {α : Type u_2} {β : Type u_3} [] [] :

An additive action of an additive monoid on a type β gives an additive action on Set β.

Equations
Instances For
def Set.mulActionSet {α : Type u_2} {β : Type u_3} [] [] :
MulAction α (Set β)

A multiplicative action of a monoid on a type β gives a multiplicative action on Set β.

Equations
• Set.mulActionSet =
Instances For
def Set.smulZeroClassSet {α : Type u_2} {β : Type u_3} [Zero β] [] :

If scalar multiplication by elements of α sends (0 : β) to zero, then the same is true for (0 : Set β).

Equations
• Set.smulZeroClassSet =
Instances For
def Set.distribSMulSet {α : Type u_2} {β : Type u_3} [] [] :

If the scalar multiplication (· • ·) : α → β → β is distributive, then so is (· • ·) : α → Set β → Set β.

Equations
• Set.distribSMulSet =
Instances For
def Set.distribMulActionSet {α : Type u_2} {β : Type u_3} [] [] [] :

A distributive multiplicative action of a monoid on an additive monoid β gives a distributive multiplicative action on Set β.

Equations
• Set.distribMulActionSet =
Instances For
def Set.mulDistribMulActionSet {α : Type u_2} {β : Type u_3} [] [] [] :

A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.

Equations
• Set.mulDistribMulActionSet =
Instances For
instance Set.instNoZeroSMulDivisors {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMul α β] [] :
Equations
• =
instance Set.noZeroSMulDivisors_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [SMul α β] [] :
Equations
• =
instance Set.instNoZeroDivisors {α : Type u_2} [Zero α] [Mul α] [] :
Equations
• =
theorem Set.image_vadd_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (f : F) (a : α) (s : Set α) :
f '' (a +ᵥ s) = f a +ᵥ f '' s
theorem Set.image_smul_distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [FunLike F α β] [] (f : F) (a : α) (s : Set α) :
f '' (a s) = f a f '' s
theorem Set.op_vadd_set_vadd_eq_vadd_vadd_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd αᵃᵒᵖ β] [VAdd β γ] [VAdd α γ] (a : α) (s : Set β) (t : Set γ) (h : ∀ (a : α) (b : β) (c : γ), +ᵥ c = b +ᵥ (a +ᵥ c)) :
+ᵥ t = s +ᵥ (a +ᵥ t)
theorem Set.op_smul_set_smul_eq_smul_smul_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul αᵐᵒᵖ β] [SMul β γ] [SMul α γ] (a : α) (s : Set β) (t : Set γ) (h : ∀ (a : α) (b : β) (c : γ), ( b) c = b a c) :
( s) t = s a t
theorem Set.smul_zero_subset {α : Type u_2} {β : Type u_3} [Zero β] [] (s : Set α) :
s 0 0
theorem Set.Nonempty.smul_zero {α : Type u_2} {β : Type u_3} [Zero β] [] {s : Set α} (hs : s.Nonempty) :
s 0 = 0
theorem Set.zero_mem_smul_set {α : Type u_2} {β : Type u_3} [Zero β] [] {t : Set β} {a : α} (h : 0 t) :
0 a t
theorem Set.zero_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [Zero β] [] {t : Set β} {a : α} [Zero α] [] (ha : a 0) :
0 a t 0 t

Note that we have neither SMulWithZero α (Set β) nor SMulWithZero (Set α) (Set β) because 0 * ∅ ≠ 0.

theorem Set.zero_smul_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [] (t : Set β) :
0 t 0
theorem Set.Nonempty.zero_smul {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [] {t : Set β} (ht : t.Nonempty) :
0 t = 0
@[simp]
theorem Set.zero_smul_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [] {s : Set β} (h : s.Nonempty) :
0 s = 0

A nonempty set is scaled by zero to the singleton set containing 0.

theorem Set.zero_smul_set_subset {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [] (s : Set β) :
0 s 0
theorem Set.subsingleton_zero_smul_set {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [] (s : Set β) :
(0 s).Subsingleton
theorem Set.zero_mem_smul_iff {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] [] {s : Set α} {t : Set β} [] :
0 s t 0 s t.Nonempty 0 t s.Nonempty
+ t = s + (a +ᵥ t)
theorem Set.op_smul_set_mul_eq_mul_smul_set {α : Type u_2} [] (a : α) (s : Set α) (t : Set α) :
* t = s * a t
theorem Set.pairwiseDisjoint_vadd_iff {α : Type u_2} [Add α] [] {s : Set α} {t : Set α} :
(s.PairwiseDisjoint fun (x : α) => x +ᵥ t) Set.InjOn (fun (p : α × α) => p.1 + p.2) (s ×ˢ t)
theorem Set.pairwiseDisjoint_smul_iff {α : Type u_2} [Mul α] [] {s : Set α} {t : Set α} :
(s.PairwiseDisjoint fun (x : α) => x t) Set.InjOn (fun (p : α × α) => p.1 * p.2) (s ×ˢ t)
@[simp]
theorem Set.vadd_mem_vadd_set_iff {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {a : α} {x : β} :
a +ᵥ x a +ᵥ s x s
@[simp]
theorem Set.smul_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {a : α} {x : β} :
a x a s x s
theorem Set.mem_vadd_set_iff_neg_vadd_mem {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {a : α} {x : β} :
x a +ᵥ A -a +ᵥ x A
theorem Set.mem_smul_set_iff_inv_smul_mem {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {a : α} {x : β} :
x a A a⁻¹ x A
theorem Set.mem_neg_vadd_set_iff {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {a : α} {x : β} :
x -a +ᵥ A a +ᵥ x A
theorem Set.mem_inv_smul_set_iff {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {a : α} {x : β} :
x a⁻¹ A a x A
theorem Set.preimage_vadd {α : Type u_2} {β : Type u_3} [] [] (a : α) (t : Set β) :
(fun (x : β) => a +ᵥ x) ⁻¹' t = -a +ᵥ t
theorem Set.preimage_smul {α : Type u_2} {β : Type u_3} [] [] (a : α) (t : Set β) :
(fun (x : β) => a x) ⁻¹' t = a⁻¹ t
theorem Set.preimage_vadd_neg {α : Type u_2} {β : Type u_3} [] [] (a : α) (t : Set β) :
(fun (x : β) => -a +ᵥ x) ⁻¹' t = a +ᵥ t
theorem Set.preimage_smul_inv {α : Type u_2} {β : Type u_3} [] [] (a : α) (t : Set β) :
(fun (x : β) => a⁻¹ x) ⁻¹' t = a t
@[simp]
theorem Set.set_vadd_subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {B : Set β} {a : α} :
a +ᵥ A a +ᵥ B A B
@[simp]
theorem Set.set_smul_subset_set_smul_iff {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {B : Set β} {a : α} :
a A a B A B
theorem Set.set_vadd_subset_iff {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {B : Set β} {a : α} :
a +ᵥ A B A -a +ᵥ B
theorem Set.set_smul_subset_iff {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {B : Set β} {a : α} :
a A B A a⁻¹ B
theorem Set.subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {B : Set β} {a : α} :
A a +ᵥ B -a +ᵥ A B
theorem Set.subset_set_smul_iff {α : Type u_2} {β : Type u_3} [] [] {A : Set β} {B : Set β} {a : α} :
A a B a⁻¹ A B
theorem Set.vadd_set_inter {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} :
a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
theorem Set.smul_set_inter {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} :
a (s t) = a s a t
theorem Set.vadd_set_iInter {α : Type u_2} {β : Type u_3} [] [] {ι : Type u_5} (a : α) (t : ιSet β) :
a +ᵥ ⋂ (i : ι), t i = ⋂ (i : ι), a +ᵥ t i
theorem Set.smul_set_iInter {α : Type u_2} {β : Type u_3} [] [] {ι : Type u_5} (a : α) (t : ιSet β) :
a ⋂ (i : ι), t i = ⋂ (i : ι), a t i
theorem Set.vadd_set_sdiff {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} :
a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
theorem Set.smul_set_sdiff {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} :
a (s \ t) = a s \ a t
theorem Set.vadd_set_symmDiff {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} :
a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)
theorem Set.smul_set_symmDiff {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} :
a symmDiff s t = symmDiff (a s) (a t)
@[simp]
theorem Set.vadd_set_univ {α : Type u_2} {β : Type u_3} [] [] {a : α} :
a +ᵥ Set.univ = Set.univ
@[simp]
theorem Set.smul_set_univ {α : Type u_2} {β : Type u_3} [] [] {a : α} :
a Set.univ = Set.univ
@[simp]
theorem Set.vadd_univ {α : Type u_2} {β : Type u_3} [] [] {s : Set α} (hs : s.Nonempty) :
s +ᵥ Set.univ = Set.univ
@[simp]
theorem Set.smul_univ {α : Type u_2} {β : Type u_3} [] [] {s : Set α} (hs : s.Nonempty) :
s Set.univ = Set.univ
theorem Set.vadd_set_compl {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {a : α} :
a +ᵥ s = (a +ᵥ s)
theorem Set.smul_set_compl {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {a : α} :
a s = (a s)
theorem Set.vadd_inter_ne_empty_iff {α : Type u_2} [] {s : Set α} {t : Set α} {x : α} :
(x +ᵥ s) t ∃ (a : α) (b : α), (a t b s) a + -b = x
theorem Set.smul_inter_ne_empty_iff {α : Type u_2} [] {s : Set α} {t : Set α} {x : α} :
x s t ∃ (a : α) (b : α), (a t b s) a * b⁻¹ = x
theorem Set.vadd_inter_ne_empty_iff' {α : Type u_2} [] {s : Set α} {t : Set α} {x : α} :
(x +ᵥ s) t ∃ (a : α) (b : α), (a t b s) a - b = x
theorem Set.smul_inter_ne_empty_iff' {α : Type u_2} [] {s : Set α} {t : Set α} {x : α} :
x s t ∃ (a : α) (b : α), (a t b s) a / b = x
theorem Set.op_vadd_inter_ne_empty_iff {α : Type u_2} [] {s : Set α} {t : Set α} {x : αᵃᵒᵖ} :
(x +ᵥ s) t ∃ (a : α) (b : α), (a s b t) -a + b =
theorem Set.op_smul_inter_ne_empty_iff {α : Type u_2} [] {s : Set α} {t : Set α} {x : αᵐᵒᵖ} :
x s t ∃ (a : α) (b : α), (a s b t) a⁻¹ * b =
@[simp]
theorem Set.iUnion_neg_vadd {α : Type u_2} {β : Type u_3} [] [] {s : Set β} :
⋃ (g : α), -g +ᵥ s = ⋃ (g : α), g +ᵥ s
@[simp]
theorem Set.iUnion_inv_smul {α : Type u_2} {β : Type u_3} [] [] {s : Set β} :
⋃ (g : α), g⁻¹ s = ⋃ (g : α), g s
theorem Set.iUnion_vadd_eq_setOf_exists {α : Type u_2} {β : Type u_3} [] [] {s : Set β} :
⋃ (g : α), g +ᵥ s = {a : β | ∃ (g : α), g +ᵥ a s}
theorem Set.iUnion_smul_eq_setOf_exists {α : Type u_2} {β : Type u_3} [] [] {s : Set β} :
⋃ (g : α), g s = {a : β | ∃ (g : α), g a s}
@[simp]
theorem Set.neg_vadd_set_distrib {α : Type u_2} [] (a : α) (s : Set α) :
-(a +ᵥ s) = +ᵥ -s
@[simp]
theorem Set.inv_smul_set_distrib {α : Type u_2} [] (a : α) (s : Set α) :
(a s)⁻¹ =
@[simp]
theorem Set.neg_op_vadd_set_distrib {α : Type u_2} [] (a : α) (s : Set α) :
-( +ᵥ s) = -a +ᵥ -s
@[simp]
theorem Set.inv_op_smul_set_distrib {α : Type u_2} [] (a : α) (s : Set α) :
@[simp]
theorem Set.vadd_set_disjoint_iff {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} :
Disjoint (a +ᵥ s) (a +ᵥ t) Disjoint s t
@[simp]
theorem Set.smul_set_disjoint_iff {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} :
Disjoint (a s) (a t) Disjoint s t
@[simp]
theorem Set.smul_mem_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) (A : Set β) (x : β) :
a x a A x A
theorem Set.mem_smul_set_iff_inv_smul_mem₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) (A : Set β) (x : β) :
x a A a⁻¹ x A
theorem Set.mem_inv_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) (A : Set β) (x : β) :
x a⁻¹ A a x A
theorem Set.preimage_smul₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) (t : Set β) :
(fun (x : β) => a x) ⁻¹' t = a⁻¹ t
theorem Set.preimage_smul_inv₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) (t : Set β) :
(fun (x : β) => a⁻¹ x) ⁻¹' t = a t
@[simp]
theorem Set.set_smul_subset_set_smul_iff₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
a A a B A B
theorem Set.set_smul_subset_iff₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
a A B A a⁻¹ B
theorem Set.subset_set_smul_iff₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
A a B a⁻¹ A B
theorem Set.smul_set_inter₀ {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
a (s t) = a s a t
theorem Set.smul_set_sdiff₀ {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
a (s \ t) = a s \ a t
theorem Set.smul_set_symmDiff₀ {α : Type u_2} {β : Type u_3} [] [] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
a symmDiff s t = symmDiff (a s) (a t)
theorem Set.smul_set_univ₀ {α : Type u_2} {β : Type u_3} [] [] {a : α} (ha : a 0) :
a Set.univ = Set.univ
theorem Set.smul_univ₀ {α : Type u_2} {β : Type u_3} [] [] {s : Set α} (hs : ¬s 0) :
s Set.univ = Set.univ
theorem Set.smul_univ₀' {α : Type u_2} {β : Type u_3} [] [] {s : Set α} (hs : s.Nontrivial) :
s Set.univ = Set.univ
@[simp]
theorem Set.inv_zero {α : Type u_2} [] :
0⁻¹ = 0
@[simp]
theorem Set.inv_smul_set_distrib₀ {α : Type u_2} [] (a : α) (s : Set α) :
(a s)⁻¹ =
@[simp]
theorem Set.inv_op_smul_set_distrib₀ {α : Type u_2} [] (a : α) (s : Set α) :
@[simp]
theorem Set.smul_set_neg {α : Type u_2} {β : Type u_3} [] [] [] (a : α) (t : Set β) :
a -t = -(a t)
@[simp]
theorem Set.smul_neg {α : Type u_2} {β : Type u_3} [] [] [] (s : Set α) (t : Set β) :
s -t = -(s t)
theorem Set.add_smul_subset {α : Type u_2} {β : Type u_3} [] [] [Module α β] (a : α) (b : α) (s : Set β) :
(a + b) s a s + b s
@[simp]
theorem Set.neg_smul_set {α : Type u_2} {β : Type u_3} [Ring α] [] [Module α β] (a : α) (t : Set β) :
-a t = -(a t)
@[simp]
theorem Set.neg_smul {α : Type u_2} {β : Type u_3} [Ring α] [] [Module α β] (s : Set α) (t : Set β) :
-s t = -(s t)