# mathlibdocumentation

data.set.pointwise.smul

# Pointwise operations of sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines pointwise algebraic operations on sets.

## Main declarations #

For sets `s` and `t` and scalar `a`:

• `s • t`: Scalar multiplication, set of all `x • y` where `x ∈ s` and `y ∈ t`.
• `s +ᵥ t`: Scalar addition, set of all `x +ᵥ y` where `x ∈ s` and `y ∈ t`.
• `s -ᵥ t`: Scalar subtraction, set of all `x -ᵥ y` where `x ∈ s` and `y ∈ t`.
• `a • s`: Scaling, set of all `a • x` where `x ∈ s`.
• `a +ᵥ s`: Translation, set of all `a +ᵥ x` where `x ∈ s`.

For `α` a semigroup/monoid, `set α` is a semigroup/monoid.

Appropriate definitions and results are also transported to the additive theory via `to_additive`.

## 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 #

@[protected]
def set.has_smul_set {α : Type u_2} {β : Type u_3} [ β] :
(set β)

The dilation of set `x • s` is defined as `{x • y | y ∈ s}` in locale `pointwise`.

Equations
@[protected]
def set.has_vadd_set {α : Type u_2} {β : Type u_3} [ β] :
(set β)

The translation of set `x +ᵥ s` is defined as `{x +ᵥ y | y ∈ s}` in locale `pointwise`.

Equations
@[protected]
def set.has_smul {α : Type u_2} {β : Type u_3} [ β] :
has_smul (set α) (set β)

The pointwise scalar multiplication of sets `s • t` is defined as `{x • y | x ∈ s, y ∈ t}` in locale `pointwise`.

Equations
@[protected]
def set.has_vadd {α : Type u_2} {β : Type u_3} [ β] :

The pointwise scalar addition of sets `s +ᵥ t` is defined as `{x +ᵥ y | x ∈ s, y ∈ t}` in locale `pointwise`.

Equations
@[simp]
theorem set.image2_smul {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
= s t
@[simp]
theorem set.image2_vadd {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
= s +ᵥ t
theorem set.image_smul_prod {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
(λ (x : α × β), x.fst x.snd) '' s ×ˢ t = s t
theorem set.mem_vadd {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} {b : β} :
b s +ᵥ t (x : α) (y : β), x s y t x +ᵥ y = b
theorem set.mem_smul {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} {b : β} :
b s t (x : α) (y : β), x s y t x y = b
theorem set.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} {a : α} {b : β} :
a s b t a +ᵥ b s +ᵥ t
theorem set.smul_mem_smul {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} {a : α} {b : β} :
a s b t a b s t
@[simp]
theorem set.empty_vadd {α : Type u_2} {β : Type u_3} [ β] {t : set β} :
@[simp]
theorem set.empty_smul {α : Type u_2} {β : Type u_3} [ β] {t : set β} :
@[simp]
theorem set.smul_empty {α : Type u_2} {β : Type u_3} [ β] {s : set α} :
@[simp]
theorem set.vadd_empty {α : Type u_2} {β : Type u_3} [ β] {s : set α} :
@[simp]
theorem set.vadd_eq_empty {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
s +ᵥ t = s = t =
@[simp]
theorem set.smul_eq_empty {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
s t = s = t =
@[simp]
theorem set.smul_nonempty {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
@[simp]
theorem set.vadd_nonempty {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
theorem set.nonempty.smul {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
theorem set.nonempty.vadd {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
theorem set.nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
theorem set.nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
theorem set.nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
theorem set.nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
@[simp]
theorem set.vadd_singleton {α : Type u_2} {β : Type u_3} [ β] {s : set α} {b : β} :
s +ᵥ {b} = (λ (_x : α), _x +ᵥ b) '' s
@[simp]
theorem set.smul_singleton {α : Type u_2} {β : Type u_3} [ β] {s : set α} {b : β} :
s {b} = (λ (_x : α), _x b) '' s
@[simp]
theorem set.singleton_smul {α : Type u_2} {β : Type u_3} [ β] {t : set β} {a : α} :
{a} t = a t
@[simp]
theorem set.singleton_vadd {α : Type u_2} {β : Type u_3} [ β] {t : set β} {a : α} :
{a} +ᵥ t = a +ᵥ t
@[simp]
theorem set.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [ β] {a : α} {b : β} :
{a} +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem set.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [ β] {a : α} {b : β} :
{a} {b} = {a b}
theorem set.smul_subset_smul {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ : set α} {t₁ t₂ : set β} :
s₁ s₂ t₁ t₂ s₁ t₁ s₂ t₂
theorem set.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ : set α} {t₁ t₂ : set β} :
s₁ s₂ t₁ t₂ s₁ +ᵥ t₁ s₂ +ᵥ t₂
theorem set.vadd_subset_vadd_left {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t₁ t₂ : set β} :
t₁ t₂ s +ᵥ t₁ s +ᵥ t₂
theorem set.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t₁ t₂ : set β} :
t₁ t₂ s t₁ s t₂
theorem set.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ : set α} {t : set β} :
s₁ s₂ s₁ +ᵥ t s₂ +ᵥ t
theorem set.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ : set α} {t : set β} :
s₁ s₂ s₁ t s₂ t
theorem set.vadd_subset_iff {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t u : set β} :
s +ᵥ t u (a : α), a s (b : β), b t a +ᵥ b u
theorem set.smul_subset_iff {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t u : set β} :
s t u (a : α), a s (b : β), b t a b u
theorem set.union_smul {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ : set α} {t : set β} :
(s₁ s₂) t = s₁ t s₂ t
theorem set.union_vadd {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ : set α} {t : set β} :
s₁ s₂ +ᵥ t = s₁ +ᵥ t (s₂ +ᵥ t)
theorem set.smul_union {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t₁ t₂ : set β} :
s (t₁ t₂) = s t₁ s t₂
theorem set.vadd_union {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t₁ t₂ : set β} :
s +ᵥ (t₁ t₂) = s +ᵥ t₁ (s +ᵥ t₂)
theorem set.inter_vadd_subset {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ : set α} {t : set β} :
s₁ s₂ +ᵥ t (s₁ +ᵥ t) (s₂ +ᵥ t)
theorem set.inter_smul_subset {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ : set α} {t : set β} :
(s₁ s₂) t s₁ t s₂ t
theorem set.vadd_inter_subset {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t₁ t₂ : set β} :
s +ᵥ t₁ t₂ (s +ᵥ t₁) (s +ᵥ t₂)
theorem set.smul_inter_subset {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t₁ t₂ : set β} :
s (t₁ t₂) s t₁ s t₂
theorem set.Union_smul_left_image {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
( (a : α) (H : a s), a t) = s t
theorem set.Union_vadd_left_image {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
( (a : α) (H : a s), a +ᵥ t) = s +ᵥ t
theorem set.Union_smul_right_image {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
( (a : β) (H : a t), (λ (_x : α), _x a) '' s) = s t
theorem set.Union_vadd_right_image {α : Type u_2} {β : Type u_3} [ β] {s : set α} {t : set β} :
( (a : β) (H : a t), (λ (_x : α), _x +ᵥ a) '' s) = s +ᵥ t
theorem set.Union_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : ι set α) (t : set β) :
( (i : ι), s i) t = (i : ι), s i t
theorem set.Union_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : ι set α) (t : set β) :
( (i : ι), s i) +ᵥ t = (i : ι), s i +ᵥ t
theorem set.smul_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : set α) (t : ι set β) :
(s (i : ι), t i) = (i : ι), s t i
theorem set.vadd_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : set α) (t : ι set β) :
(s +ᵥ (i : ι), t i) = (i : ι), s +ᵥ t i
theorem set.Union₂_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : Π (i : ι), κ i set α) (t : set β) :
( (i : ι) (j : κ i), s i j) t = (i : ι) (j : κ i), s i j t
theorem set.Union₂_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : Π (i : ι), κ i set α) (t : set β) :
( (i : ι) (j : κ i), s i j) +ᵥ t = (i : ι) (j : κ i), s i j +ᵥ t
theorem set.vadd_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : set α) (t : Π (i : ι), κ i set β) :
(s +ᵥ (i : ι) (j : κ i), t i j) = (i : ι) (j : κ i), s +ᵥ t i j
theorem set.smul_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : set α) (t : Π (i : ι), κ i set β) :
(s (i : ι) (j : κ i), t i j) = (i : ι) (j : κ i), s t i j
theorem set.Inter_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : ι set α) (t : set β) :
( (i : ι), s i) +ᵥ t (i : ι), s i +ᵥ t
theorem set.Inter_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : ι set α) (t : set β) :
( (i : ι), s i) t (i : ι), s i t
theorem set.vadd_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : set α) (t : ι set β) :
(s +ᵥ (i : ι), t i) (i : ι), s +ᵥ t i
theorem set.smul_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : set α) (t : ι set β) :
(s (i : ι), t i) (i : ι), s t i
theorem set.Inter₂_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : Π (i : ι), κ i set α) (t : set β) :
( (i : ι) (j : κ i), s i j) +ᵥ t (i : ι) (j : κ i), s i j +ᵥ t
theorem set.Inter₂_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : Π (i : ι), κ i set α) (t : set β) :
( (i : ι) (j : κ i), s i j) t (i : ι) (j : κ i), s i j t
theorem set.vadd_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : set α) (t : Π (i : ι), κ i set β) :
(s +ᵥ (i : ι) (j : κ i), t i j) (i : ι) (j : κ i), s +ᵥ t i j
theorem set.smul_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : set α) (t : Π (i : ι), κ i set β) :
(s (i : ι) (j : κ i), t i j) (i : ι) (j : κ i), s t i j
@[simp]
theorem set.bUnion_smul_set {α : Type u_2} {β : Type u_3} [ β] (s : set α) (t : set β) :
( (a : α) (H : a s), a t) = s t
@[simp]
theorem set.bUnion_vadd_set {α : Type u_2} {β : Type u_3} [ β] (s : set α) (t : set β) :
( (a : α) (H : a s), a +ᵥ t) = s +ᵥ t
@[simp]
theorem set.image_vadd {α : Type u_2} {β : Type u_3} [ β] {t : set β} {a : α} :
(λ (x : β), a +ᵥ x) '' t = a +ᵥ t
@[simp]
theorem set.image_smul {α : Type u_2} {β : Type u_3} [ β] {t : set β} {a : α} :
(λ (x : β), a x) '' t = a t
theorem set.mem_vadd_set {α : Type u_2} {β : Type u_3} [ β] {t : set β} {a : α} {x : β} :
x a +ᵥ t (y : β), y t a +ᵥ y = x
theorem set.mem_smul_set {α : Type u_2} {β : Type u_3} [ β] {t : set β} {a : α} {x : β} :
x a t (y : β), y t a y = x
theorem set.smul_mem_smul_set {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} {b : β} :
b s a b a s
theorem set.vadd_mem_vadd_set {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} {b : β} :
b s a +ᵥ b a +ᵥ s
@[simp]
theorem set.smul_set_empty {α : Type u_2} {β : Type u_3} [ β] {a : α} :
@[simp]
theorem set.vadd_set_empty {α : Type u_2} {β : Type u_3} [ β] {a : α} :
@[simp]
theorem set.smul_set_eq_empty {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
a s = s =
@[simp]
theorem set.vadd_set_eq_empty {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
a +ᵥ s = s =
@[simp]
theorem set.smul_set_nonempty {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
@[simp]
theorem set.vadd_set_nonempty {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
@[simp]
theorem set.vadd_set_singleton {α : Type u_2} {β : Type u_3} [ β] {a : α} {b : β} :
a +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem set.smul_set_singleton {α : Type u_2} {β : Type u_3} [ β] {a : α} {b : β} :
a {b} = {a b}
theorem set.vadd_set_mono {α : Type u_2} {β : Type u_3} [ β] {s t : set β} {a : α} :
s t a +ᵥ s a +ᵥ t
theorem set.smul_set_mono {α : Type u_2} {β : Type u_3} [ β] {s t : set β} {a : α} :
s t a s a t
theorem set.vadd_set_subset_iff {α : Type u_2} {β : Type u_3} [ β] {s t : set β} {a : α} :
a +ᵥ s t ⦃b : β⦄, b s a +ᵥ b t
theorem set.smul_set_subset_iff {α : Type u_2} {β : Type u_3} [ β] {s t : set β} {a : α} :
a s t ⦃b : β⦄, b s a b t
theorem set.vadd_set_union {α : Type u_2} {β : Type u_3} [ β] {t₁ t₂ : set β} {a : α} :
a +ᵥ (t₁ t₂) = a +ᵥ t₁ (a +ᵥ t₂)
theorem set.smul_set_union {α : Type u_2} {β : Type u_3} [ β] {t₁ t₂ : set β} {a : α} :
a (t₁ t₂) = a t₁ a t₂
theorem set.smul_set_inter_subset {α : Type u_2} {β : Type u_3} [ β] {t₁ t₂ : set β} {a : α} :
a (t₁ t₂) a t₁ a t₂
theorem set.vadd_set_inter_subset {α : Type u_2} {β : Type u_3} [ β] {t₁ t₂ : set β} {a : α} :
a +ᵥ t₁ t₂ (a +ᵥ t₁) (a +ᵥ t₂)
theorem set.vadd_set_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (a : α) (s : ι set β) :
(a +ᵥ (i : ι), s i) = (i : ι), a +ᵥ s i
theorem set.smul_set_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (a : α) (s : ι set β) :
(a (i : ι), s i) = (i : ι), a s i
theorem set.smul_set_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (a : α) (s : Π (i : ι), κ i set β) :
(a (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), a s i j
theorem set.vadd_set_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (a : α) (s : Π (i : ι), κ i set β) :
(a +ᵥ (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), a +ᵥ s i j
theorem set.vadd_set_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (a : α) (t : ι set β) :
(a +ᵥ (i : ι), t i) (i : ι), a +ᵥ t i
theorem set.smul_set_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (a : α) (t : ι set β) :
(a (i : ι), t i) (i : ι), a t i
theorem set.vadd_set_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (a : α) (t : Π (i : ι), κ i set β) :
(a +ᵥ (i : ι) (j : κ i), t i j) (i : ι) (j : κ i), a +ᵥ t i j
theorem set.smul_set_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (a : α) (t : Π (i : ι), κ i set β) :
(a (i : ι) (j : κ i), t i j) (i : ι) (j : κ i), a t i j
theorem set.nonempty.vadd_set {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
theorem set.nonempty.smul_set {α : Type u_2} {β : Type u_3} [ β] {s : set β} {a : α} :
@[simp]
theorem set.bUnion_op_vadd_set {α : Type u_2} [has_add α] (s t : set α) :
( (a : α) (H : a t), = s + t
@[simp]
theorem set.bUnion_op_smul_set {α : Type u_2} [has_mul α] (s t : set α) :
( (a : α) (H : a t), s) = s * t
theorem set.range_vadd_range {α : Type u_2} {β : Type u_3} {ι : Type u_1} {κ : Type u_4} [ β] (b : ι α) (c : κ β) :
= set.range (λ (p : ι × κ), b p.fst +ᵥ c p.snd)
theorem set.range_smul_range {α : Type u_2} {β : Type u_3} {ι : Type u_1} {κ : Type u_4} [ β] (b : ι α) (c : κ β) :
= set.range (λ (p : ι × κ), b p.fst c p.snd)
theorem set.smul_set_range {α : Type u_2} {β : Type u_3} {a : α} [ β] {ι : Sort u_1} {f : ι β} :
a = set.range (λ (i : ι), a f i)
theorem set.vadd_set_range {α : Type u_2} {β : Type u_3} {a : α} [ β] {ι : Sort u_1} {f : ι β} :
a +ᵥ = set.range (λ (i : ι), a +ᵥ f i)
@[protected, instance]
def set.vadd_comm_class_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(set γ)
@[protected, instance]
def set.smul_comm_class_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(set γ)
@[protected, instance]
def set.vadd_comm_class_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.smul_comm_class_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.smul_comm_class_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
β (set γ)
@[protected, instance]
def set.vadd_comm_class_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
β (set γ)
@[protected, instance]
def set.vadd_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.smul_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.is_scalar_tower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(set γ)
@[protected, instance]
def set.vadd_assoc_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(set γ)
@[protected, instance]
def set.vadd_assoc_class' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.vadd_assoc_class'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ β] [ γ] [ γ] [ γ] :
(set β) (set γ)
@[protected, instance]
def set.is_central_scalar {α : Type u_2} {β : Type u_3} [ β] [ β] [ β] :
(set β)
@[protected]
def set.mul_action {α : Type u_2} {β : Type u_3} [monoid α] [ β] :
mul_action (set α) (set β)

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

Equations
@[protected]
def set.add_action {α : Type u_2} {β : Type u_3} [add_monoid α] [ β] :

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

Equations
@[protected]
def set.add_action_set {α : Type u_2} {β : Type u_3} [add_monoid α] [ β] :
(set β)

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

Equations
@[protected]
def set.mul_action_set {α : Type u_2} {β : Type u_3} [monoid α] [ β] :
(set β)

A multiplicative action of a monoid on a type `β` gives a multiplicative action on `set β`.

Equations
@[protected]
def set.distrib_mul_action_set {α : Type u_2} {β : Type u_3} [monoid α] [add_monoid β] [ β] :
(set β)

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

Equations
@[protected]
def set.mul_distrib_mul_action_set {α : Type u_2} {β : Type u_3} [monoid α] [monoid β]  :

A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `set β`.

Equations
@[protected, instance]
def set.no_zero_smul_divisors {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β]  :
(set β)
@[protected, instance]
def set.no_zero_smul_divisors_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β]  :
(set β)
@[protected, instance]
def set.no_zero_divisors {α : Type u_2} [has_zero α] [has_mul α]  :
@[protected, instance]
def set.has_vsub {α : Type u_2} {β : Type u_3} [ β] :
has_vsub (set α) (set β)
Equations
@[simp]
theorem set.image2_vsub {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
= s -ᵥ t
theorem set.image_vsub_prod {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
(λ (x : β × β), x.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t
theorem set.mem_vsub {α : Type u_2} {β : Type u_3} [ β] {s t : set β} {a : α} :
a s -ᵥ t (x y : β), x s y t x -ᵥ y = a
theorem set.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [ β] {s t : set β} {b c : β} (hb : b s) (hc : c t) :
b -ᵥ c s -ᵥ t
@[simp]
theorem set.empty_vsub {α : Type u_2} {β : Type u_3} [ β] (t : set β) :
@[simp]
theorem set.vsub_empty {α : Type u_2} {β : Type u_3} [ β] (s : set β) :
@[simp]
theorem set.vsub_eq_empty {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
s -ᵥ t = s = t =
@[simp]
theorem set.vsub_nonempty {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
theorem set.nonempty.vsub {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
theorem set.nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
theorem set.nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
@[simp]
theorem set.vsub_singleton {α : Type u_2} {β : Type u_3} [ β] (s : set β) (b : β) :
s -ᵥ {b} = (λ (_x : β), _x -ᵥ b) '' s
@[simp]
theorem set.singleton_vsub {α : Type u_2} {β : Type u_3} [ β] (t : set β) (b : β) :
{b} -ᵥ t =
@[simp]
theorem set.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [ β] {b c : β} :
{b} -ᵥ {c} = {b -ᵥ c}
theorem set.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ t₁ t₂ : set β} :
s₁ s₂ t₁ t₂ s₁ -ᵥ t₁ s₂ -ᵥ t₂
theorem set.vsub_subset_vsub_left {α : Type u_2} {β : Type u_3} [ β] {s t₁ t₂ : set β} :
t₁ t₂ s -ᵥ t₁ s -ᵥ t₂
theorem set.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ t : set β} :
s₁ s₂ s₁ -ᵥ t s₂ -ᵥ t
theorem set.vsub_subset_iff {α : Type u_2} {β : Type u_3} [ β] {s t : set β} {u : set α} :
s -ᵥ t u (x : β), x s (y : β), y t x -ᵥ y u
theorem set.vsub_self_mono {α : Type u_2} {β : Type u_3} [ β] {s t : set β} (h : s t) :
s -ᵥ s t -ᵥ t
theorem set.union_vsub {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ t : set β} :
s₁ s₂ -ᵥ t = s₁ -ᵥ t (s₂ -ᵥ t)
theorem set.vsub_union {α : Type u_2} {β : Type u_3} [ β] {s t₁ t₂ : set β} :
s -ᵥ (t₁ t₂) = s -ᵥ t₁ (s -ᵥ t₂)
theorem set.inter_vsub_subset {α : Type u_2} {β : Type u_3} [ β] {s₁ s₂ t : set β} :
s₁ s₂ -ᵥ t (s₁ -ᵥ t) (s₂ -ᵥ t)
theorem set.vsub_inter_subset {α : Type u_2} {β : Type u_3} [ β] {s t₁ t₂ : set β} :
s -ᵥ t₁ t₂ (s -ᵥ t₁) (s -ᵥ t₂)
theorem set.Union_vsub_left_image {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
( (a : β) (H : a s), '' t) = s -ᵥ t
theorem set.Union_vsub_right_image {α : Type u_2} {β : Type u_3} [ β] {s t : set β} :
( (a : β) (H : a t), (λ (_x : β), _x -ᵥ a) '' s) = s -ᵥ t
theorem set.Union_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : ι set β) (t : set β) :
( (i : ι), s i) -ᵥ t = (i : ι), s i -ᵥ t
theorem set.vsub_Union {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : set β) (t : ι set β) :
(s -ᵥ (i : ι), t i) = (i : ι), s -ᵥ t i
theorem set.Union₂_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : Π (i : ι), κ i set β) (t : set β) :
( (i : ι) (j : κ i), s i j) -ᵥ t = (i : ι) (j : κ i), s i j -ᵥ t
theorem set.vsub_Union₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : set β) (t : Π (i : ι), κ i set β) :
(s -ᵥ (i : ι) (j : κ i), t i j) = (i : ι) (j : κ i), s -ᵥ t i j
theorem set.Inter_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : ι set β) (t : set β) :
( (i : ι), s i) -ᵥ t (i : ι), s i -ᵥ t
theorem set.vsub_Inter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [ β] (s : set β) (t : ι set β) :
(s -ᵥ (i : ι), t i) (i : ι), s -ᵥ t i
theorem set.Inter₂_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : Π (i : ι), κ i set β) (t : set β) :
( (i : ι) (j : κ i), s i j) -ᵥ t (i : ι) (j : κ i), s i j -ᵥ t
theorem set.vsub_Inter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι Sort u_6} [ β] (s : set β) (t : Π (i : ι), κ i set β) :
(s -ᵥ (i : ι) (j : κ i), t i j) (i : ι) (j : κ i), s -ᵥ t i j

Note that we have neither `smul_with_zero α (set β)` nor `smul_with_zero (set α) (set β)` because `0 * ∅ ≠ 0`.

theorem set.smul_zero_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] (s : set α) :
s 0 0
theorem set.zero_smul_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] (t : set β) :
0 t 0
theorem set.nonempty.smul_zero {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {s : set α} (hs : s.nonempty) :
s 0 = 0
theorem set.nonempty.zero_smul {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {t : set β} (ht : t.nonempty) :
0 t = 0
theorem set.zero_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_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} [has_zero α] [has_zero β] [ β] (s : set β) :
0 s 0
theorem set.subsingleton_zero_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] (s : set β) :
theorem set.zero_mem_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {t : set β} {a : α} (h : 0 t) :
0 a t
theorem set.zero_mem_smul_iff {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {s : set α} {t : set β}  :
0 s t 0 s t.nonempty 0 t s.nonempty
theorem set.zero_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [ β] {t : set β} {a : α} (ha : a 0) :
0 a t 0 t
theorem set.pairwise_disjoint_smul_iff {α : Type u_2} {s t : set α} :
s.pairwise_disjoint (λ (_x : α), _x t) set.inj_on (λ (p : α × α), p.fst * p.snd) (s ×ˢ t)
theorem set.pairwise_disjoint_vadd_iff {α : Type u_2} {s t : set α} :
s.pairwise_disjoint (λ (_x : α), _x +ᵥ t) set.inj_on (λ (p : α × α), p.fst + p.snd) (s ×ˢ t)
@[simp]
theorem set.vadd_mem_vadd_set_iff {α : Type u_2} {β : Type u_3} [add_group α] [ β] {s : set β} {a : α} {x : β} :
a +ᵥ x a +ᵥ s x s
@[simp]
theorem set.smul_mem_smul_set_iff {α : Type u_2} {β : Type u_3} [group α] [ β] {s : set β} {a : α} {x : β} :
a x a s x s
theorem set.mem_smul_set_iff_inv_smul_mem {α : Type u_2} {β : Type u_3} [group α] [ β] {A : set β} {a : α} {x : β} :
x a A a⁻¹ x A
theorem set.mem_vadd_set_iff_neg_vadd_mem {α : Type u_2} {β : Type u_3} [add_group α] [ β] {A : set β} {a : α} {x : β} :
x a +ᵥ A -a +ᵥ x A
theorem set.mem_inv_smul_set_iff {α : Type u_2} {β : Type u_3} [group α] [ β] {A : set β} {a : α} {x : β} :
x a⁻¹ A a x A
theorem set.mem_neg_vadd_set_iff {α : Type u_2} {β : Type u_3} [add_group α] [ β] {A : set β} {a : α} {x : β} :
x -a +ᵥ A a +ᵥ x A
theorem set.preimage_smul {α : Type u_2} {β : Type u_3} [group α] [ β] (a : α) (t : set β) :
(λ (x : β), a x) ⁻¹' t = a⁻¹ t
theorem set.preimage_vadd {α : Type u_2} {β : Type u_3} [add_group α] [ β] (a : α) (t : set β) :
(λ (x : β), a +ᵥ x) ⁻¹' t = -a +ᵥ t
theorem set.preimage_smul_inv {α : Type u_2} {β : Type u_3} [group α] [ β] (a : α) (t : set β) :
(λ (x : β), a⁻¹ x) ⁻¹' t = a t
theorem set.preimage_vadd_neg {α : Type u_2} {β : Type u_3} [add_group α] [ β] (a : α) (t : set β) :
(λ (x : β), -a +ᵥ x) ⁻¹' t = a +ᵥ t
@[simp]
theorem set.set_vadd_subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [add_group α] [ β] {A B : set β} {a : α} :
a +ᵥ A a +ᵥ B A B
@[simp]
theorem set.set_smul_subset_set_smul_iff {α : Type u_2} {β : Type u_3} [group α] [ β] {A B : set β} {a : α} :
a A a B A B
theorem set.set_smul_subset_iff {α : Type u_2} {β : Type u_3} [group α] [ β] {A B : set β} {a : α} :
a A B A a⁻¹ B
theorem set.set_vadd_subset_iff {α : Type u_2} {β : Type u_3} [add_group α] [ β] {A B : set β} {a : α} :
a +ᵥ A B A -a +ᵥ B
theorem set.subset_set_smul_iff {α : Type u_2} {β : Type u_3} [group α] [ β] {A B : set β} {a : α} :
A a B a⁻¹ A B
theorem set.subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [add_group α] [ β] {A B : set β} {a : α} :
A a +ᵥ B -a +ᵥ A B
theorem set.vadd_set_inter {α : Type u_2} {β : Type u_3} [add_group α] [ β] {s t : set β} {a : α} :
a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
theorem set.smul_set_inter {α : Type u_2} {β : Type u_3} [group α] [ β] {s t : set β} {a : α} :
a (s t) = a s a t
theorem set.vadd_set_sdiff {α : Type u_2} {β : Type u_3} [add_group α] [ β] {s t : set β} {a : α} :
a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
theorem set.smul_set_sdiff {α : Type u_2} {β : Type u_3} [group α] [ β] {s t : set β} {a : α} :
a (s \ t) = a s \ a t
theorem set.vadd_set_symm_diff {α : Type u_2} {β : Type u_3} [add_group α] [ β] {s t : set β} {a : α} :
a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
theorem set.smul_set_symm_diff {α : Type u_2} {β : Type u_3} [group α] [ β] {s t : set β} {a : α} :
a s t = (a s) (a t)
@[simp]
theorem set.smul_set_univ {α : Type u_2} {β : Type u_3} [group α] [ β] {a : α} :
@[simp]
theorem set.vadd_set_univ {α : Type u_2} {β : Type u_3} [add_group α] [ β] {a : α} :
@[simp]
theorem set.vadd_univ {α : Type u_2} {β : Type u_3} [add_group α] [ β] {s : set α} (hs : s.nonempty) :
@[simp]
theorem set.smul_univ {α : Type u_2} {β : Type u_3} [group α] [ β] {s : set α} (hs : s.nonempty) :
theorem set.vadd_inter_ne_empty_iff {α : Type u_2} [add_group α] {s 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} [group α] {s 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} [group α] {s 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} [add_group α] {s t : set α} {x : α} :
(x +ᵥ s) t (a b : α), (a t b s) a - b = x
theorem set.op_smul_inter_ne_empty_iff {α : Type u_2} [group α] {s t : set α} {x : αᵐᵒᵖ} :
x s t (a b : α), (a s b t) a⁻¹ * b =
theorem set.op_vadd_inter_ne_empty_iff {α : Type u_2} [add_group α] {s t : set α} {x : αᵃᵒᵖ} :
(x +ᵥ s) t (a b : α), (a s b t) -a + b =
@[simp]
theorem set.Union_neg_vadd {α : Type u_2} {β : Type u_3} [add_group α] [ β] {s : set β} :
( (g : α), -g +ᵥ s) = (g : α), g +ᵥ s
@[simp]
theorem set.Union_inv_smul {α : Type u_2} {β : Type u_3} [group α] [ β] {s : set β} :
( (g : α), g⁻¹ s) = (g : α), g s
theorem set.Union_smul_eq_set_of_exists {α : Type u_2} {β : Type u_3} [group α] [ β] {s : set β} :
( (g : α), g s) = {a : β | (g : α), g a s}
theorem set.Union_vadd_eq_set_of_exists {α : Type u_2} {β : Type u_3} [add_group α] [ β] {s : set β} :
( (g : α), g +ᵥ s) = {a : β | (g : α), g +ᵥ a s}
@[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 β) :
(λ (x : β), a x) ⁻¹' t = a⁻¹ t
theorem set.preimage_smul_inv₀ {α : Type u_2} {β : Type u_3} [ β] {a : α} (ha : a 0) (t : set β) :
(λ (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 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 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 B : set β} :
A a B a⁻¹ A B
theorem set.smul_set_inter₀ {α : Type u_2} {β : Type u_3} [ β] {s 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 t : set β} {a : α} (ha : a 0) :
a (s \ t) = a s \ a t
theorem set.smul_set_symm_diff₀ {α : Type u_2} {β : Type u_3} [ β] {s t : set β} {a : α} (ha : a 0) :
a s t = (a s) (a t)
theorem set.smul_set_univ₀ {α : Type u_2} {β : Type u_3} [ β] {a : α} (ha : a 0) :
theorem set.smul_univ₀ {α : Type u_2} {β : Type u_3} [ β] {s : set α} (hs : ¬s 0) :
theorem set.smul_univ₀' {α : Type u_2} {β : Type u_3} [ β] {s : set α} (hs : s.nontrivial) :
@[simp]
theorem set.smul_set_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [ β] (a : α) (t : set β) :
a -t = -(a t)
@[protected, simp]
theorem set.smul_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [ β] (s : set α) (t : set β) :
s -t = -(s t)
@[simp]
theorem set.neg_smul_set {α : Type u_2} {β : Type u_3} [ring α] [ β] (a : α) (t : set β) :
-a t = -(a t)
@[protected, simp]
theorem set.neg_smul {α : Type u_2} {β : Type u_3} [ring α] [ β] (s : set α) (t : set β) :
-s t = -(s t)