mathlib documentation

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:

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 #

Translation/scaling of sets #

@[protected]
def set.has_smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] :
has_smul α (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} [has_vadd α β] :
has_vadd α (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 α β] :
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} [has_vadd α β] :
has_vadd (set α) (set β)

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} [has_smul α β] {s : set α} {t : set β} :
@[simp]
theorem set.image2_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
theorem set.image_smul_prod {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
(λ (x : α × β), x.fst x.snd) '' s ×ˢ t = s t
theorem set.mem_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {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} [has_smul α β] {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} [has_vadd α β] {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} [has_smul α β] {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} [has_vadd α β] {t : set β} :
@[simp]
theorem set.empty_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {t : set β} :
@[simp]
theorem set.smul_empty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} :
@[simp]
theorem set.vadd_empty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} :
@[simp]
theorem set.vadd_eq_empty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
s +ᵥ t = s = t =
@[simp]
theorem set.smul_eq_empty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
s t = s = t =
@[simp]
theorem set.smul_nonempty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
@[simp]
theorem set.vadd_nonempty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
theorem set.nonempty.smul {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
theorem set.nonempty.vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
theorem set.nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
theorem set.nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
theorem set.nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
theorem set.nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
@[simp]
theorem set.vadd_singleton {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {b : β} :
s +ᵥ {b} = (λ (_x : α), _x +ᵥ b) '' s
@[simp]
theorem set.smul_singleton {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {b : β} :
s {b} = (λ (_x : α), _x b) '' s
@[simp]
theorem set.singleton_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {t : set β} {a : α} :
{a} t = a t
@[simp]
theorem set.singleton_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {t : set β} {a : α} :
{a} +ᵥ t = a +ᵥ t
@[simp]
theorem set.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [has_vadd α β] {a : α} {b : β} :
{a} +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem set.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [has_smul α β] {a : α} {b : β} :
{a} {b} = {a b}
theorem set.smul_subset_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {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} [has_vadd α β] {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} [has_vadd α β] {s : set α} {t₁ t₂ : set β} :
t₁ t₂ s +ᵥ t₁ s +ᵥ t₂
theorem set.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t₁ t₂ : set β} :
t₁ t₂ s t₁ s t₂
theorem set.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [has_vadd α β] {s₁ s₂ : set α} {t : set β} :
s₁ s₂ s₁ +ᵥ t s₂ +ᵥ t
theorem set.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [has_smul α β] {s₁ s₂ : set α} {t : set β} :
s₁ s₂ s₁ t s₂ t
theorem set.vadd_subset_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {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} [has_smul α β] {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} [has_smul α β] {s₁ s₂ : set α} {t : set β} :
(s₁ s₂) t = s₁ t s₂ t
theorem set.union_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {s₁ s₂ : set α} {t : set β} :
s₁ s₂ +ᵥ t = s₁ +ᵥ t (s₂ +ᵥ t)
theorem set.smul_union {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t₁ t₂ : set β} :
s (t₁ t₂) = s t₁ s t₂
theorem set.vadd_union {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t₁ t₂ : set β} :
s +ᵥ (t₁ t₂) = s +ᵥ t₁ (s +ᵥ t₂)
theorem set.inter_vadd_subset {α : Type u_2} {β : Type u_3} [has_vadd α β] {s₁ s₂ : set α} {t : set β} :
s₁ s₂ +ᵥ t (s₁ +ᵥ t) (s₂ +ᵥ t)
theorem set.inter_smul_subset {α : Type u_2} {β : Type u_3} [has_smul α β] {s₁ s₂ : set α} {t : set β} :
(s₁ s₂) t s₁ t s₂ t
theorem set.vadd_inter_subset {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t₁ t₂ : set β} :
s +ᵥ t₁ t₂ (s +ᵥ t₁) (s +ᵥ t₂)
theorem set.smul_inter_subset {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t₁ t₂ : set β} :
s (t₁ t₂) s t₁ s t₂
theorem set.Union_smul_left_image {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set α} {t : set β} :
( (a : α) (H : a s), a t) = s t
theorem set.Union_vadd_left_image {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set α} {t : set β} :
( (a : α) (H : a s), a +ᵥ t) = s +ᵥ t
theorem set.Union_smul_right_image {α : Type u_2} {β : Type u_3} [has_smul α β] {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} [has_vadd α β] {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} [has_smul α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_vadd α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_smul α β] (s : set α) (t : set β) :
( (a : α) (H : a s), a t) = s t
@[simp]
theorem set.bUnion_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] (s : set α) (t : set β) :
( (a : α) (H : a s), a +ᵥ t) = s +ᵥ t
@[simp]
theorem set.image_vadd {α : Type u_2} {β : Type u_3} [has_vadd α β] {t : set β} {a : α} :
(λ (x : β), a +ᵥ x) '' t = a +ᵥ t
@[simp]
theorem set.image_smul {α : Type u_2} {β : Type u_3} [has_smul α β] {t : set β} {a : α} :
(λ (x : β), a x) '' t = a t
theorem set.mem_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {t : set β} {a : α} {x : β} :
x a +ᵥ t (y : β), y t a +ᵥ y = x
theorem set.mem_smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {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} [has_smul α β] {s : set β} {a : α} {b : β} :
b s a b a s
theorem set.vadd_mem_vadd_set {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} {b : β} :
b s a +ᵥ b a +ᵥ s
@[simp]
theorem set.smul_set_empty {α : Type u_2} {β : Type u_3} [has_smul α β] {a : α} :
@[simp]
theorem set.vadd_set_empty {α : Type u_2} {β : Type u_3} [has_vadd α β] {a : α} :
@[simp]
theorem set.smul_set_eq_empty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :
a s = s =
@[simp]
theorem set.vadd_set_eq_empty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :
a +ᵥ s = s =
@[simp]
theorem set.smul_set_nonempty {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :
@[simp]
theorem set.vadd_set_nonempty {α : Type u_2} {β : Type u_3} [has_vadd α β] {s : set β} {a : α} :
@[simp]
theorem set.vadd_set_singleton {α : Type u_2} {β : Type u_3} [has_vadd α β] {a : α} {b : β} :
a +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem set.smul_set_singleton {α : Type u_2} {β : Type u_3} [has_smul α β] {a : α} {b : β} :
a {b} = {a b}
theorem set.vadd_set_mono {α : Type u_2} {β : Type u_3} [has_vadd α β] {s t : set β} {a : α} :
s t a +ᵥ s a +ᵥ t
theorem set.smul_set_mono {α : Type u_2} {β : Type u_3} [has_smul α β] {s t : set β} {a : α} :
s t a s a t
theorem set.vadd_set_subset_iff {α : Type u_2} {β : Type u_3} [has_vadd α β] {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} [has_smul α β] {s t : set β} {a : α} :
a s t ⦃b : β⦄, b s a b t
theorem set.vadd_set_union {α : Type u_2} {β : Type u_3} [has_vadd α β] {t₁ t₂ : set β} {a : α} :
a +ᵥ (t₁ t₂) = a +ᵥ t₁ (a +ᵥ t₂)
theorem set.smul_set_union {α : Type u_2} {β : Type u_3} [has_smul α β] {t₁ t₂ : set β} {a : α} :
a (t₁ t₂) = a t₁ a t₂
theorem set.smul_set_inter_subset {α : Type u_2} {β : Type u_3} [has_smul α β] {t₁ t₂ : set β} {a : α} :
a (t₁ t₂) a t₁ a t₂
theorem set.vadd_set_inter_subset {α : Type u_2} {β : Type u_3} [has_vadd α β] {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} [has_vadd α β] (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} [has_smul α β] (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} [has_smul α β] (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} [has_vadd α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_vadd α β] (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} [has_smul α β] (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} [has_vadd α β] {s : set β} {a : α} :
theorem set.nonempty.smul_set {α : Type u_2} {β : Type u_3} [has_smul α β] {s : set β} {a : α} :
@[simp]
theorem set.bUnion_op_vadd_set {α : Type u_2} [has_add α] (s t : set α) :
( (a : α) (H : a t), add_opposite.op a +ᵥ s) = s + t
@[simp]
theorem set.bUnion_op_smul_set {α : Type u_2} [has_mul α] (s t : set α) :
( (a : α) (H : a t), mul_opposite.op a s) = s * t
theorem set.range_vadd_range {α : Type u_2} {β : Type u_3} {ι : Type u_1} {κ : Type u_4} [has_vadd α β] (b : ι α) (c : κ β) :
set.range b +ᵥ set.range 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} [has_smul α β] (b : ι α) (c : κ β) :
set.range b set.range c = set.range (λ (p : ι × κ), b p.fst c p.snd)
theorem set.smul_set_range {α : Type u_2} {β : Type u_3} {a : α} [has_smul α β] {ι : Sort u_1} {f : ι β} :
a set.range f = set.range (λ (i : ι), a f i)
theorem set.vadd_set_range {α : Type u_2} {β : Type u_3} {a : α} [has_vadd α β] {ι : Sort u_1} {f : ι β} :
a +ᵥ set.range f = set.range (λ (i : ι), a +ᵥ f i)
@[protected, instance]
def set.vadd_comm_class_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class α β (set γ)
@[protected, instance]
def set.smul_comm_class_set {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class α β (set γ)
@[protected, instance]
def set.vadd_comm_class_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class α (set β) (set γ)
@[protected, instance]
def set.smul_comm_class_set' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class α (set β) (set γ)
@[protected, instance]
def set.smul_comm_class_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class (set α) β (set γ)
@[protected, instance]
def set.vadd_comm_class_set'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class (set α) β (set γ)
@[protected, instance]
def set.vadd_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α γ] [has_vadd β γ] [vadd_comm_class α β γ] :
vadd_comm_class (set α) (set β) (set γ)
@[protected, instance]
def set.smul_comm_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α γ] [has_smul β γ] [smul_comm_class α β γ] :
smul_comm_class (set α) (set β) (set γ)
@[protected, instance]
def set.is_scalar_tower {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower α β (set γ)
@[protected, instance]
def set.vadd_assoc_class {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
@[protected, instance]
def set.vadd_assoc_class' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
vadd_assoc_class α (set β) (set γ)
@[protected, instance]
def set.is_scalar_tower' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower α (set β) (set γ)
@[protected, instance]
def set.vadd_assoc_class'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd α β] [has_vadd α γ] [has_vadd β γ] [vadd_assoc_class α β γ] :
vadd_assoc_class (set α) (set β) (set γ)
@[protected, instance]
def set.is_scalar_tower'' {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_smul α β] [has_smul α γ] [has_smul β γ] [is_scalar_tower α β γ] :
is_scalar_tower (set α) (set β) (set γ)
@[protected, instance]
def set.is_central_scalar {α : Type u_2} {β : Type u_3} [has_smul α β] [has_smul αᵐᵒᵖ β] [is_central_scalar α β] :
@[protected]
def set.mul_action {α : Type u_2} {β : Type u_3} [monoid α] [mul_action α β] :
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 α] [add_action α β] :
add_action (set α) (set β)

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 α] [add_action α β] :
add_action α (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 α] [mul_action α β] :
mul_action α (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 β] [distrib_mul_action α β] :

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

Equations
@[protected]

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 β] [has_smul α β] [no_zero_smul_divisors α β] :
@[protected, instance]
def set.no_zero_smul_divisors_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [has_smul α β] [no_zero_smul_divisors α β] :
@[protected, instance]
@[protected, instance]
def set.has_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] :
has_vsub (set α) (set β)
Equations
@[simp]
theorem set.image2_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :
theorem set.image_vsub_prod {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :
(λ (x : β × β), x.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t
theorem set.mem_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {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} [has_vsub α β] {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} [has_vsub α β] (t : set β) :
@[simp]
theorem set.vsub_empty {α : Type u_2} {β : Type u_3} [has_vsub α β] (s : set β) :
@[simp]
theorem set.vsub_eq_empty {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :
s -ᵥ t = s = t =
@[simp]
theorem set.vsub_nonempty {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :
theorem set.nonempty.vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :
theorem set.nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :
theorem set.nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :
@[simp]
theorem set.vsub_singleton {α : Type u_2} {β : Type u_3} [has_vsub α β] (s : set β) (b : β) :
s -ᵥ {b} = (λ (_x : β), _x -ᵥ b) '' s
@[simp]
theorem set.singleton_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] (t : set β) (b : β) :
@[simp]
theorem set.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [has_vsub α β] {b c : β} :
{b} -ᵥ {c} = {b -ᵥ c}
theorem set.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {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} [has_vsub α β] {s t₁ t₂ : set β} :
t₁ t₂ s -ᵥ t₁ s -ᵥ t₂
theorem set.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [has_vsub α β] {s₁ s₂ t : set β} :
s₁ s₂ s₁ -ᵥ t s₂ -ᵥ t
theorem set.vsub_subset_iff {α : Type u_2} {β : Type u_3} [has_vsub α β] {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} [has_vsub α β] {s t : set β} (h : s t) :
s -ᵥ s t -ᵥ t
theorem set.union_vsub {α : Type u_2} {β : Type u_3} [has_vsub α β] {s₁ s₂ t : set β} :
s₁ s₂ -ᵥ t = s₁ -ᵥ t (s₂ -ᵥ t)
theorem set.vsub_union {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t₁ t₂ : set β} :
s -ᵥ (t₁ t₂) = s -ᵥ t₁ (s -ᵥ t₂)
theorem set.inter_vsub_subset {α : Type u_2} {β : Type u_3} [has_vsub α β] {s₁ s₂ t : set β} :
s₁ s₂ -ᵥ t (s₁ -ᵥ t) (s₂ -ᵥ t)
theorem set.vsub_inter_subset {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t₁ t₂ : set β} :
s -ᵥ t₁ t₂ (s -ᵥ t₁) (s -ᵥ t₂)
theorem set.Union_vsub_left_image {α : Type u_2} {β : Type u_3} [has_vsub α β] {s t : set β} :
( (a : β) (H : a s), has_vsub.vsub a '' t) = s -ᵥ t
theorem set.Union_vsub_right_image {α : Type u_2} {β : Type u_3} [has_vsub α β] {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} [has_vsub α β] (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} [has_vsub α β] (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} [has_vsub α β] (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} [has_vsub α β] (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} [has_vsub α β] (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} [has_vsub α β] (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} [has_vsub α β] (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} [has_vsub α β] (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 β] [smul_with_zero α β] (s : set α) :
s 0 0
theorem set.zero_smul_subset {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] (t : set β) :
0 t 0
theorem set.nonempty.smul_zero {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {s : set α} (hs : s.nonempty) :
s 0 = 0
theorem set.nonempty.zero_smul {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] {t : set β} (ht : t.nonempty) :
0 t = 0
theorem set.zero_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_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 β] [smul_with_zero α β] (s : set β) :
0 s 0
theorem set.subsingleton_zero_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_zero α β] (s : set β) :
theorem set.zero_mem_smul_set {α : Type u_2} {β : Type u_3} [has_zero α] [has_zero β] [smul_with_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 β] [smul_with_zero α β] {s : set α} {t : set β} [no_zero_smul_divisors α β] :
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 β] [smul_with_zero α β] {t : set β} [no_zero_smul_divisors α β] {a : α} (ha : a 0) :
0 a t 0 t
theorem set.pairwise_disjoint_smul_iff {α : Type u_2} [left_cancel_semigroup α] {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} [add_left_cancel_semigroup α] {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 α] [add_action α β] {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 α] [mul_action α β] {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 α] [mul_action α β] {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 α] [add_action α β] {A : set β} {a : α} {x : β} :
x a +ᵥ A -a +ᵥ x A
theorem set.mem_inv_smul_set_iff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {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 α] [add_action α β] {A : set β} {a : α} {x : β} :
x -a +ᵥ A a +ᵥ x A
theorem set.preimage_smul {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] (a : α) (t : set β) :
(λ (x : β), a x) ⁻¹' t = a⁻¹ t
theorem set.preimage_vadd {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] (a : α) (t : set β) :
(λ (x : β), a +ᵥ x) ⁻¹' t = -a +ᵥ t
theorem set.preimage_smul_inv {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] (a : α) (t : set β) :
(λ (x : β), a⁻¹ x) ⁻¹' t = a t
theorem set.preimage_vadd_neg {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] (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 α] [add_action α β] {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 α] [mul_action α β] {A B : set β} {a : α} :
a A a B A B
theorem set.set_smul_subset_iff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {A B : set β} {a : α} :
a A B A a⁻¹ B
theorem set.set_vadd_subset_iff {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {A B : set β} {a : α} :
a +ᵥ A B A -a +ᵥ B
theorem set.subset_set_smul_iff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {A B : set β} {a : α} :
A a B a⁻¹ A B
theorem set.subset_set_vadd_iff {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {A B : set β} {a : α} :
A a +ᵥ B -a +ᵥ A B
theorem set.vadd_set_inter {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {s t : set β} {a : α} :
a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
theorem set.smul_set_inter {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {s t : set β} {a : α} :
a (s t) = a s a t
theorem set.vadd_set_sdiff {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {s t : set β} {a : α} :
a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
theorem set.smul_set_sdiff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {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 α] [add_action α β] {s t : set β} {a : α} :
a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
theorem set.smul_set_symm_diff {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {s t : set β} {a : α} :
a s t = (a s) (a t)
@[simp]
theorem set.smul_set_univ {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {a : α} :
@[simp]
theorem set.vadd_set_univ {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {a : α} :
@[simp]
theorem set.vadd_univ {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {s : set α} (hs : s.nonempty) :
@[simp]
theorem set.smul_univ {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {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 = mul_opposite.unop x
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 = add_opposite.unop x
@[simp]
theorem set.Union_neg_vadd {α : Type u_2} {β : Type u_3} [add_group α] [add_action α β] {s : set β} :
( (g : α), -g +ᵥ s) = (g : α), g +ᵥ s
@[simp]
theorem set.Union_inv_smul {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {s : set β} :
( (g : α), g⁻¹ s) = (g : α), g s
theorem set.Union_smul_eq_set_of_exists {α : Type u_2} {β : Type u_3} [group α] [mul_action α β] {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 α] [add_action α β] {s : set β} :
( (g : α), g +ᵥ s) = {a : β | (g : α), g +ᵥ a s}
@[simp]
theorem set.smul_mem_smul_set_iff₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {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} [group_with_zero α] [mul_action α β] {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} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) (A : set β) (x : β) :
x a⁻¹ A a x A
theorem set.preimage_smul₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) (t : set β) :
(λ (x : β), a x) ⁻¹' t = a⁻¹ t
theorem set.preimage_smul_inv₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {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} [group_with_zero α] [mul_action α β] {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} [group_with_zero α] [mul_action α β] {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} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) {A B : set β} :
A a B a⁻¹ A B
theorem set.smul_set_inter₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {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} [group_with_zero α] [mul_action α β] {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} [group_with_zero α] [mul_action α β] {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} [group_with_zero α] [mul_action α β] {a : α} (ha : a 0) :
theorem set.smul_univ₀ {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {s : set α} (hs : ¬s 0) :
theorem set.smul_univ₀' {α : Type u_2} {β : Type u_3} [group_with_zero α] [mul_action α β] {s : set α} (hs : s.nontrivial) :
@[simp]
theorem set.smul_set_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [distrib_mul_action α β] (a : α) (t : set β) :
a -t = -(a t)
@[protected, simp]
theorem set.smul_neg {α : Type u_2} {β : Type u_3} [monoid α] [add_group β] [distrib_mul_action α β] (s : set α) (t : set β) :
s -t = -(s t)
@[simp]
theorem set.neg_smul_set {α : Type u_2} {β : Type u_3} [ring α] [add_comm_group β] [module α β] (a : α) (t : set β) :
-a t = -(a t)
@[protected, simp]
theorem set.neg_smul {α : Type u_2} {β : Type u_3} [ring α] [add_comm_group β] [module α β] (s : set α) (t : set β) :
-s t = -(s t)