Documentation

Mathlib.Data.Set.Pointwise.SMul

Pointwise operations of sets #

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 #

def Set.vaddSet {α : Type u_1} {β : Type u_2} [inst : VAdd α β] :
VAdd α (Set β)

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

Equations
def Set.smulSet {α : Type u_1} {β : Type u_2} [inst : SMul α β] :
SMul α (Set β)

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

Equations
def Set.vadd {α : Type u_1} {β : Type u_2} [inst : VAdd α β] :
VAdd (Set α) (Set β)

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

Equations
def Set.smul {α : Type u_1} {β : Type u_2} [inst : SMul α β] :
SMul (Set α) (Set β)

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

Equations
@[simp]
theorem Set.image2_vadd {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t : Set β} :
Set.image2 VAdd.vadd s t = s +ᵥ t
@[simp]
theorem Set.image2_smul {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} :
Set.image2 SMul.smul s t = s t
theorem Set.image_smul_prod {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} :
(fun x => x.fst x.snd) '' s ×ˢ t = s t
theorem Set.mem_vadd {α : Type u_2} {β : Type u_1} [inst : 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_1} [inst : 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_1} {β : Type u_2} [inst : VAdd α β] {s : Set α} {t : Set β} {a : α} {b : β} :
a sb ta +ᵥ b s +ᵥ t
theorem Set.smul_mem_smul {α : Type u_1} {β : Type u_2} [inst : SMul α β] {s : Set α} {t : Set β} {a : α} {b : β} :
a sb ta b s t
@[simp]
theorem Set.empty_vadd {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {t : Set β} :
@[simp]
theorem Set.empty_smul {α : Type u_2} {β : Type u_1} [inst : SMul α β] {t : Set β} :
@[simp]
theorem Set.vadd_empty {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} :
@[simp]
theorem Set.smul_empty {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} :
@[simp]
theorem Set.vadd_eq_empty {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t : Set β} :
s +ᵥ t = s = t =
@[simp]
theorem Set.smul_eq_empty {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} :
s t = s = t =
@[simp]
theorem Set.vadd_nonempty {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t : Set β} :
@[simp]
theorem Set.smul_nonempty {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} :
theorem Set.Nonempty.vadd {α : Type u_1} {β : Type u_2} [inst : VAdd α β] {s : Set α} {t : Set β} :
theorem Set.Nonempty.smul {α : Type u_1} {β : Type u_2} [inst : SMul α β] {s : Set α} {t : Set β} :
theorem Set.Nonempty.of_vadd_left {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t : Set β} :
theorem Set.Nonempty.of_smul_left {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} :
theorem Set.Nonempty.of_vadd_right {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t : Set β} :
theorem Set.Nonempty.of_smul_right {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} :
@[simp]
theorem Set.vadd_singleton {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {b : β} :
s +ᵥ {b} = (fun x => x +ᵥ b) '' s
@[simp]
theorem Set.smul_singleton {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {b : β} :
s {b} = (fun x => x b) '' s
@[simp]
theorem Set.singleton_vadd {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {t : Set β} {a : α} :
{a} +ᵥ t = a +ᵥ t
@[simp]
theorem Set.singleton_smul {α : Type u_2} {β : Type u_1} [inst : SMul α β] {t : Set β} {a : α} :
{a} t = a t
@[simp]
theorem Set.singleton_vadd_singleton {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {a : α} {b : β} :
{a} +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem Set.singleton_smul_singleton {α : Type u_2} {β : Type u_1} [inst : SMul α β] {a : α} {b : β} :
{a} {b} = {a b}
theorem Set.vadd_subset_vadd {α : Type u_1} {β : Type u_2} [inst : VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
s₁ s₂t₁ t₂s₁ +ᵥ t₁ s₂ +ᵥ t₂
theorem Set.smul_subset_smul {α : Type u_1} {β : Type u_2} [inst : SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
s₁ s₂t₁ t₂s₁ t₁ s₂ t₂
theorem Set.vadd_subset_vadd_left {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
t₁ t₂s +ᵥ t₁ s +ᵥ t₂
theorem Set.smul_subset_smul_left {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
t₁ t₂s t₁ s t₂
theorem Set.vadd_subset_vadd_right {α : Type u_1} {β : Type u_2} [inst : VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
s₁ s₂s₁ +ᵥ t s₂ +ᵥ t
theorem Set.smul_subset_smul_right {α : Type u_1} {β : Type u_2} [inst : SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
s₁ s₂s₁ t s₂ t
theorem Set.vadd_subset_iff {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t : Set β} {u : Set β} :
s +ᵥ t u ∀ (a : α), a s∀ (b : β), b ta +ᵥ b u
theorem Set.smul_subset_iff {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} {u : Set β} :
s t u ∀ (a : α), a s∀ (b : β), b ta b u
theorem Set.union_vadd {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
s₁ s₂ +ᵥ t = s₁ +ᵥ t (s₂ +ᵥ t)
theorem Set.union_smul {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
(s₁ s₂) t = s₁ t s₂ t
theorem Set.vadd_union {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
s +ᵥ (t₁ t₂) = s +ᵥ t₁ (s +ᵥ t₂)
theorem Set.smul_union {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
s (t₁ t₂) = s t₁ s t₂
theorem Set.inter_vadd_subset {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
s₁ s₂ +ᵥ t (s₁ +ᵥ t) (s₂ +ᵥ t)
theorem Set.inter_smul_subset {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} :
(s₁ s₂) t s₁ t s₂ t
theorem Set.vadd_inter_subset {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
s +ᵥ t₁ t₂ (s +ᵥ t₁) (s +ᵥ t₂)
theorem Set.smul_inter_subset {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} :
s (t₁ t₂) s t₁ s t₂
theorem Set.unionᵢ_vadd_left_image {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t : Set β} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => a +ᵥ t) = s +ᵥ t
theorem Set.unionᵢ_smul_left_image {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => a t) = s t
theorem Set.unionᵢ_vadd_right_image {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set α} {t : Set β} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x +ᵥ a) '' s) = s +ᵥ t
theorem Set.unionᵢ_smul_right_image {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set α} {t : Set β} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x a) '' s) = s t
theorem Set.unionᵢ_vadd {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : VAdd α β] (s : ιSet α) (t : Set β) :
(Set.unionᵢ fun i => s i) +ᵥ t = Set.unionᵢ fun i => s i +ᵥ t
theorem Set.unionᵢ_smul {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SMul α β] (s : ιSet α) (t : Set β) :
(Set.unionᵢ fun i => s i) t = Set.unionᵢ fun i => s i t
theorem Set.vadd_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : VAdd α β] (s : Set α) (t : ιSet β) :
(s +ᵥ Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s +ᵥ t i
theorem Set.smul_unionᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SMul α β] (s : Set α) (t : ιSet β) :
(s Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s t i
theorem Set.unionᵢ₂_vadd {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} [inst : VAdd α β] (s : (i : ι) → κ iSet α) (t : Set β) :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) +ᵥ t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j +ᵥ t
theorem Set.unionᵢ₂_smul {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} [inst : SMul α β] (s : (i : ι) → κ iSet α) (t : Set β) :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j t
theorem Set.vadd_unionᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} [inst : VAdd α β] (s : Set α) (t : (i : ι) → κ iSet β) :
(s +ᵥ Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s +ᵥ t i j
theorem Set.smul_unionᵢ₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} [inst : SMul α β] (s : Set α) (t : (i : ι) → κ iSet β) :
(s Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s t i j
theorem Set.interᵢ_vadd_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : VAdd α β] (s : ιSet α) (t : Set β) :
(Set.interᵢ fun i => s i) +ᵥ t Set.interᵢ fun i => s i +ᵥ t
theorem Set.interᵢ_smul_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SMul α β] (s : ιSet α) (t : Set β) :
(Set.interᵢ fun i => s i) t Set.interᵢ fun i => s i t
theorem Set.vadd_interᵢ_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : VAdd α β] (s : Set α) (t : ιSet β) :
(s +ᵥ Set.interᵢ fun i => t i) Set.interᵢ fun i => s +ᵥ t i
theorem Set.smul_interᵢ_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SMul α β] (s : Set α) (t : ιSet β) :
(s Set.interᵢ fun i => t i) Set.interᵢ fun i => s t i
theorem Set.interᵢ₂_vadd_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} [inst : VAdd α β] (s : (i : ι) → κ iSet α) (t : Set β) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) +ᵥ t Set.interᵢ fun i => Set.interᵢ fun j => s i j +ᵥ t
theorem Set.interᵢ₂_smul_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} [inst : SMul α β] (s : (i : ι) → κ iSet α) (t : Set β) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) t Set.interᵢ fun i => Set.interᵢ fun j => s i j t
theorem Set.vadd_interᵢ₂_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} [inst : VAdd α β] (s : Set α) (t : (i : ι) → κ iSet β) :
(s +ᵥ Set.interᵢ fun i => Set.interᵢ fun j => t i j) Set.interᵢ fun i => Set.interᵢ fun j => s +ᵥ t i j
theorem Set.smul_interᵢ₂_subset {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {κ : ιSort u_4} [inst : SMul α β] (s : Set α) (t : (i : ι) → κ iSet β) :
(s Set.interᵢ fun i => Set.interᵢ fun j => t i j) Set.interᵢ fun i => Set.interᵢ fun j => s t i j
@[simp]
theorem Set.unionᵢ_vadd_set {α : Type u_1} {β : Type u_2} [inst : VAdd α β] (s : Set α) (t : Set β) :
(Set.unionᵢ fun a => Set.unionᵢ fun h => a +ᵥ t) = s +ᵥ t
@[simp]
theorem Set.unionᵢ_smul_set {α : Type u_1} {β : Type u_2} [inst : SMul α β] (s : Set α) (t : Set β) :
(Set.unionᵢ fun a => Set.unionᵢ fun h => a t) = s t
@[simp]
theorem Set.image_vadd {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {t : Set β} {a : α} :
(fun x => a +ᵥ x) '' t = a +ᵥ t
@[simp]
theorem Set.image_smul {α : Type u_2} {β : Type u_1} [inst : SMul α β] {t : Set β} {a : α} :
(fun x => a x) '' t = a t
theorem Set.mem_vadd_set {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {t : Set β} {a : α} {x : β} :
x a +ᵥ t y, y t a +ᵥ y = x
theorem Set.mem_smul_set {α : Type u_2} {β : Type u_1} [inst : SMul α β] {t : Set β} {a : α} {x : β} :
x a t y, y t a y = x
theorem Set.vadd_mem_vadd_set {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α} {b : β} :
b sa +ᵥ b a +ᵥ s
theorem Set.smul_mem_smul_set {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {a : α} {b : β} :
b sa b a s
@[simp]
theorem Set.vadd_set_empty {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {a : α} :
@[simp]
theorem Set.smul_set_empty {α : Type u_2} {β : Type u_1} [inst : SMul α β] {a : α} :
@[simp]
theorem Set.vadd_set_eq_empty {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α} :
a +ᵥ s = s =
@[simp]
theorem Set.smul_set_eq_empty {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {a : α} :
a s = s =
@[simp]
theorem Set.vadd_set_nonempty {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α} :
@[simp]
theorem Set.smul_set_nonempty {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {a : α} :
@[simp]
theorem Set.vadd_set_singleton {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {a : α} {b : β} :
a +ᵥ {b} = {a +ᵥ b}
@[simp]
theorem Set.smul_set_singleton {α : Type u_2} {β : Type u_1} [inst : SMul α β] {a : α} {b : β} :
a {b} = {a b}
theorem Set.vadd_set_mono {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {t : Set β} {a : α} :
s ta +ᵥ s a +ᵥ t
theorem Set.smul_set_mono {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {t : Set β} {a : α} :
s ta s a t
theorem Set.vadd_set_subset_iff {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {t : Set β} {a : α} :
a +ᵥ s t ∀ ⦃b : β⦄, b sa +ᵥ b t
theorem Set.smul_set_subset_iff {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {t : Set β} {a : α} :
a s t ∀ ⦃b : β⦄, b sa b t
theorem Set.vadd_set_union {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {t₁ : Set β} {t₂ : Set β} {a : α} :
a +ᵥ (t₁ t₂) = a +ᵥ t₁ (a +ᵥ t₂)
theorem Set.smul_set_union {α : Type u_2} {β : Type u_1} [inst : SMul α β] {t₁ : Set β} {t₂ : Set β} {a : α} :
a (t₁ t₂) = a t₁ a t₂
theorem Set.vadd_set_inter_subset {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {t₁ : Set β} {t₂ : Set β} {a : α} :
a +ᵥ t₁ t₂ (a +ᵥ t₁) (a +ᵥ t₂)
theorem Set.smul_set_inter_subset {α : Type u_2} {β : Type u_1} [inst : SMul α β] {t₁ : Set β} {t₂ : Set β} {a : α} :
a (t₁ t₂) a t₁ a t₂
theorem Set.vadd_set_Union {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : VAdd α β] (a : α) (s : ιSet β) :
(a +ᵥ Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => a +ᵥ s i
theorem Set.smul_set_Union {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : SMul α β] (a : α) (s : ιSet β) :
(a Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => a s i
theorem Set.vadd_set_unionᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : VAdd α β] (a : α) (s : (i : ι) → κ iSet β) :
(a +ᵥ Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => a +ᵥ s i j
theorem Set.smul_set_unionᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : SMul α β] (a : α) (s : (i : ι) → κ iSet β) :
(a Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => a s i j
theorem Set.vadd_set_interᵢ_subset {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : VAdd α β] (a : α) (t : ιSet β) :
(a +ᵥ Set.interᵢ fun i => t i) Set.interᵢ fun i => a +ᵥ t i
theorem Set.smul_set_interᵢ_subset {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : SMul α β] (a : α) (t : ιSet β) :
(a Set.interᵢ fun i => t i) Set.interᵢ fun i => a t i
theorem Set.vadd_set_interᵢ₂_subset {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : VAdd α β] (a : α) (t : (i : ι) → κ iSet β) :
(a +ᵥ Set.interᵢ fun i => Set.interᵢ fun j => t i j) Set.interᵢ fun i => Set.interᵢ fun j => a +ᵥ t i j
theorem Set.smul_set_interᵢ₂_subset {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : SMul α β] (a : α) (t : (i : ι) → κ iSet β) :
(a Set.interᵢ fun i => Set.interᵢ fun j => t i j) Set.interᵢ fun i => Set.interᵢ fun j => a t i j
theorem Set.Nonempty.vadd_set {α : Type u_2} {β : Type u_1} [inst : VAdd α β] {s : Set β} {a : α} :
theorem Set.Nonempty.smul_set {α : Type u_2} {β : Type u_1} [inst : SMul α β] {s : Set β} {a : α} :
@[simp]
theorem Set.unionᵢ_op_vadd_set {α : Type u_1} [inst : Add α] (s : Set α) (t : Set α) :
(Set.unionᵢ fun a => Set.unionᵢ fun h => { unop := a } +ᵥ s) = s + t
@[simp]
theorem Set.unionᵢ_op_smul_set {α : Type u_1} [inst : Mul α] (s : Set α) (t : Set α) :
(Set.unionᵢ fun a => Set.unionᵢ fun h => { unop := a } s) = s * t
abbrev Set.range_vadd_range.match_2 {α : Type u_4} {β : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : VAdd α β] (b : ια) (c : κβ) (_x : β) (motive : (_x Set.range fun p => b p.fst +ᵥ c p.snd) → Prop) :
(x : _x Set.range fun p => b p.fst +ᵥ c p.snd) → ((i : ι) → (j : κ) → (h : (fun p => b p.fst +ᵥ c p.snd) (i, j) = _x) → motive (_ : y, (fun p => b p.fst +ᵥ c p.snd) y = _x)) → motive x
Equations
  • One or more equations did not get rendered due to their size.
abbrev Set.range_vadd_range.match_1 {α : Type u_1} {β : Type u_2} {ι : Type u_3} {κ : Type u_4} [inst : VAdd α β] (b : ια) (c : κβ) (_x : β) (motive : (x y, x Set.range b y Set.range c x +ᵥ y = _x) → Prop) :
(x : x y, x Set.range b y Set.range c x +ᵥ y = _x) → ((_p : α) → (_q : β) → (i : ι) → (hi : b i = _p) → (j : κ) → (hj : c j = _q) → (hpq : _p +ᵥ _q = _x) → motive (_ : x y, x Set.range b y Set.range c x +ᵥ y = _x)) → motive x
Equations
  • One or more equations did not get rendered due to their size.
theorem Set.range_vadd_range {α : Type u_3} {β : Type u_4} {ι : Type u_1} {κ : Type u_2} [inst : VAdd α β] (b : ια) (c : κβ) :
Set.range b +ᵥ Set.range c = Set.range fun p => b p.fst +ᵥ c p.snd
theorem Set.range_smul_range {α : Type u_3} {β : Type u_4} {ι : Type u_1} {κ : Type u_2} [inst : SMul α β] (b : ια) (c : κβ) :
Set.range b Set.range c = Set.range fun p => b p.fst c p.snd
theorem Set.vadd_set_range {α : Type u_1} {β : Type u_2} {a : α} [inst : VAdd α β] {ι : Sort u_3} {f : ιβ} :
a +ᵥ Set.range f = Set.range fun i => a +ᵥ f i
theorem Set.smul_set_range {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] {ι : Sort u_3} {f : ιβ} :
a Set.range f = Set.range fun i => a f i
def Set.vaddCommClass_set.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :
VAddCommClass α β (Set γ)
Equations
instance Set.vaddCommClass_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :
VAddCommClass α β (Set γ)
Equations
instance Set.smulCommClass_set {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α γ] [inst : SMul β γ] [inst : SMulCommClass α β γ] :
SMulCommClass α β (Set γ)
Equations
instance Set.vaddCommClass_set' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :
VAddCommClass α (Set β) (Set γ)
Equations
def Set.vaddCommClass_set'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :
VAddCommClass α (Set β) (Set γ)
Equations
instance Set.smulCommClass_set' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α γ] [inst : SMul β γ] [inst : SMulCommClass α β γ] :
SMulCommClass α (Set β) (Set γ)
Equations
def Set.vaddCommClass_set''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :
VAddCommClass (Set α) β (Set γ)
Equations
instance Set.vaddCommClass_set'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :
VAddCommClass (Set α) β (Set γ)
Equations
instance Set.smulCommClass_set'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α γ] [inst : SMul β γ] [inst : SMulCommClass α β γ] :
SMulCommClass (Set α) β (Set γ)
Equations
def Set.vaddCommClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :
VAddCommClass (Set α) (Set β) (Set γ)
Equations
instance Set.vaddCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddCommClass α β γ] :
VAddCommClass (Set α) (Set β) (Set γ)
Equations
instance Set.smulCommClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α γ] [inst : SMul β γ] [inst : SMulCommClass α β γ] :
SMulCommClass (Set α) (Set β) (Set γ)
Equations
def Set.vAddAssocClass.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :
VAddAssocClass α β (Set γ)
Equations
instance Set.vAddAssocClass {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :
VAddAssocClass α β (Set γ)
Equations
instance Set.isScalarTower {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α β] [inst : SMul α γ] [inst : SMul β γ] [inst : IsScalarTower α β γ] :
IsScalarTower α β (Set γ)
Equations
def Set.vAddAssocClass'.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :
VAddAssocClass α (Set β) (Set γ)
Equations
instance Set.vAddAssocClass' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :
VAddAssocClass α (Set β) (Set γ)
Equations
instance Set.isScalarTower' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α β] [inst : SMul α γ] [inst : SMul β γ] [inst : IsScalarTower α β γ] :
IsScalarTower α (Set β) (Set γ)
Equations
def Set.vAddAssocClass''.proof_1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :
VAddAssocClass (Set α) (Set β) (Set γ)
Equations
instance Set.vAddAssocClass'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β γ] [inst : VAddAssocClass α β γ] :
VAddAssocClass (Set α) (Set β) (Set γ)
Equations
instance Set.isScalarTower'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α β] [inst : SMul α γ] [inst : SMul β γ] [inst : IsScalarTower α β γ] :
IsScalarTower (Set α) (Set β) (Set γ)
Equations
def Set.isCentralVAdd.proof_1 {α : Type u_1} {β : Type u_2} [inst : VAdd α β] [inst : VAdd αᵃᵒᵖ β] [inst : IsCentralVAdd α β] :
Equations
instance Set.isCentralVAdd {α : Type u_1} {β : Type u_2} [inst : VAdd α β] [inst : VAdd αᵃᵒᵖ β] [inst : IsCentralVAdd α β] :
Equations
instance Set.isCentralScalar {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst : SMul αᵐᵒᵖ β] [inst : IsCentralScalar α β] :
Equations
def Set.addAction.proof_2 {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst : AddAction α β] :
∀ (x x_1 : Set α) (x_2 : Set β), Set.image2 (fun x x_3 => x +ᵥ x_3) (Set.image2 (fun x x_3 => x + x_3) x x_1) x_2 = Set.image2 (fun x x_3 => x +ᵥ x_3) x (Set.image2 (fun x x_3 => x +ᵥ x_3) x_1 x_2)
Equations
  • One or more equations did not get rendered due to their size.
def Set.addAction.proof_1 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] (s : Set β) :
Set.image2 (fun x x_1 => x +ᵥ x_1) {0} s = s
Equations
def Set.addAction {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst : AddAction α β] :
AddAction (Set α) (Set β)

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

Equations
  • One or more equations did not get rendered due to their size.
def Set.mulAction {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : MulAction α β] :
MulAction (Set α) (Set β)

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

Equations
  • One or more equations did not get rendered due to their size.
def Set.addActionSet {α : Type u_1} {β : Type u_2} [inst : AddMonoid α] [inst : AddAction α β] :
AddAction α (Set β)

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

Equations
  • One or more equations did not get rendered due to their size.
def Set.addActionSet.proof_2 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] :
∀ (x y : α) (b : Set β), (fun x_1 => x + y +ᵥ x_1) '' b = (fun x_1 => x +ᵥ x_1) '' ((fun x => y +ᵥ x) '' b)
Equations
def Set.addActionSet.proof_1 {α : Type u_2} {β : Type u_1} [inst : AddMonoid α] [inst : AddAction α β] :
∀ (b : Set β), (fun x => 0 +ᵥ x) '' b = b
Equations
def Set.mulActionSet {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : MulAction α β] :
MulAction α (Set β)

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

Equations
  • One or more equations did not get rendered due to their size.
def Set.distribMulActionSet {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : AddMonoid β] [inst : DistribMulAction α β] :

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

Equations
  • One or more equations did not get rendered due to their size.
def Set.mulDistribMulActionSet {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst : Monoid β] [inst : MulDistribMulAction α β] :

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

Equations
  • One or more equations did not get rendered due to their size.
instance Set.noZeroSMulDivisors_set {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Zero β] [inst : SMul α β] [inst : NoZeroSMulDivisors α β] :
Equations
instance Set.vsub {α : Type u_1} {β : Type u_2} [inst : VSub α β] :
VSub (Set α) (Set β)
Equations
@[simp]
theorem Set.image2_vsub {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} :
Set.image2 VSub.vsub s t = s -ᵥ t
theorem Set.image_vsub_prod {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} :
(fun x => x.fst -ᵥ x.snd) '' s ×ˢ t = s -ᵥ t
theorem Set.mem_vsub {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {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_1} [inst : VSub α β] {s : Set β} {t : Set β} {b : β} {c : β} (hb : b s) (hc : c t) :
b -ᵥ c s -ᵥ t
@[simp]
theorem Set.empty_vsub {α : Type u_2} {β : Type u_1} [inst : VSub α β] (t : Set β) :
@[simp]
theorem Set.vsub_empty {α : Type u_2} {β : Type u_1} [inst : VSub α β] (s : Set β) :
@[simp]
theorem Set.vsub_eq_empty {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} :
s -ᵥ t = s = t =
@[simp]
theorem Set.vsub_nonempty {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} :
theorem Set.Nonempty.vsub {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s : Set β} {t : Set β} :
theorem Set.Nonempty.of_vsub_left {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} :
theorem Set.Nonempty.of_vsub_right {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} :
@[simp]
theorem Set.vsub_singleton {α : Type u_2} {β : Type u_1} [inst : VSub α β] (s : Set β) (b : β) :
s -ᵥ {b} = (fun x => x -ᵥ b) '' s
@[simp]
theorem Set.singleton_vsub {α : Type u_2} {β : Type u_1} [inst : VSub α β] (t : Set β) (b : β) :
{b} -ᵥ t = (fun x x_1 => x -ᵥ x_1) b '' t
@[simp]
theorem Set.singleton_vsub_singleton {α : Type u_1} {β : Type u_2} [inst : VSub α β] {b : β} {c : β} :
{b} -ᵥ {c} = {b -ᵥ c}
theorem Set.vsub_subset_vsub {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} :
s₁ s₂t₁ t₂s₁ -ᵥ t₁ s₂ -ᵥ t₂
theorem Set.vsub_subset_vsub_left {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} :
t₁ t₂s -ᵥ t₁ s -ᵥ t₂
theorem Set.vsub_subset_vsub_right {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} :
s₁ s₂s₁ -ᵥ t s₂ -ᵥ t
theorem Set.vsub_subset_iff {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} {u : Set α} :
s -ᵥ t u ∀ (x : β), x s∀ (y : β), y tx -ᵥ y u
theorem Set.vsub_self_mono {α : Type u_2} {β : Type u_1} [inst : VSub α β] {s : Set β} {t : Set β} (h : s t) :
s -ᵥ s t -ᵥ t
theorem Set.union_vsub {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} :
s₁ s₂ -ᵥ t = s₁ -ᵥ t (s₂ -ᵥ t)
theorem Set.vsub_union {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} :
s -ᵥ (t₁ t₂) = s -ᵥ t₁ (s -ᵥ t₂)
theorem Set.inter_vsub_subset {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} :
s₁ s₂ -ᵥ t (s₁ -ᵥ t) (s₂ -ᵥ t)
theorem Set.vsub_inter_subset {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} :
s -ᵥ t₁ t₂ (s -ᵥ t₁) (s -ᵥ t₂)
theorem Set.unionᵢ_vsub_left_image {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x x_1 => x -ᵥ x_1) a '' t) = s -ᵥ t
theorem Set.unionᵢ_vsub_right_image {α : Type u_1} {β : Type u_2} [inst : VSub α β] {s : Set β} {t : Set β} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x -ᵥ a) '' s) = s -ᵥ t
theorem Set.unionᵢ_vsub {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : VSub α β] (s : ιSet β) (t : Set β) :
(Set.unionᵢ fun i => s i) -ᵥ t = Set.unionᵢ fun i => s i -ᵥ t
theorem Set.vsub_unionᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : VSub α β] (s : Set β) (t : ιSet β) :
(s -ᵥ Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s -ᵥ t i
theorem Set.unionᵢ₂_vsub {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : VSub α β] (s : (i : ι) → κ iSet β) (t : Set β) :
(Set.unionᵢ fun i => Set.unionᵢ fun j => s i j) -ᵥ t = Set.unionᵢ fun i => Set.unionᵢ fun j => s i j -ᵥ t
theorem Set.vsub_unionᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : VSub α β] (s : Set β) (t : (i : ι) → κ iSet β) :
(s -ᵥ Set.unionᵢ fun i => Set.unionᵢ fun j => t i j) = Set.unionᵢ fun i => Set.unionᵢ fun j => s -ᵥ t i j
theorem Set.interᵢ_vsub_subset {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : VSub α β] (s : ιSet β) (t : Set β) :
(Set.interᵢ fun i => s i) -ᵥ t Set.interᵢ fun i => s i -ᵥ t
theorem Set.vsub_interᵢ_subset {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : VSub α β] (s : Set β) (t : ιSet β) :
(s -ᵥ Set.interᵢ fun i => t i) Set.interᵢ fun i => s -ᵥ t i
theorem Set.interᵢ₂_vsub_subset {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : VSub α β] (s : (i : ι) → κ iSet β) (t : Set β) :
(Set.interᵢ fun i => Set.interᵢ fun j => s i j) -ᵥ t Set.interᵢ fun i => Set.interᵢ fun j => s i j -ᵥ t
theorem Set.vsub_interᵢ₂_subset {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : VSub α β] (s : Set β) (t : (i : ι) → κ iSet β) :
(s -ᵥ Set.interᵢ fun i => Set.interᵢ fun j => t i j) Set.interᵢ fun i => Set.interᵢ fun j => s -ᵥ t i j
theorem Set.image_vadd_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : VAdd α β] [inst : VAdd α γ] (f : βγ) (a : α) (s : Set β) :
(∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → f '' (a +ᵥ s) = a +ᵥ f '' s
theorem Set.image_smul_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SMul α β] [inst : SMul α γ] (f : βγ) (a : α) (s : Set β) :
(∀ (b : β), f (a b) = a f b) → f '' (a s) = a f '' s
theorem Set.image_vadd_distrib {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : AddZeroClass α] [inst : AddZeroClass β] [inst : AddMonoidHomClass F α β] (f : F) (a : α) (s : Set α) :
f '' (a +ᵥ s) = f a +ᵥ f '' s
theorem Set.image_smul_distrib {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst : MulOneClass β] [inst : MonoidHomClass F α β] (f : F) (a : α) (s : Set α) :
f '' (a s) = f a f '' s

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

theorem Set.smul_zero_subset {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] (s : Set α) :
s 0 0
theorem Set.zero_smul_subset {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] (t : Set β) :
0 t 0
theorem Set.Nonempty.smul_zero {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {s : Set α} (hs : Set.Nonempty s) :
s 0 = 0
theorem Set.Nonempty.zero_smul {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {t : Set β} (ht : Set.Nonempty t) :
0 t = 0
theorem Set.zero_smul_set {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {s : Set β} (h : Set.Nonempty s) :
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_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] (s : Set β) :
0 s 0
theorem Set.subsingleton_zero_smul_set {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] (s : Set β) :
theorem Set.zero_mem_smul_set {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {t : Set β} {a : α} (h : 0 t) :
0 a t
theorem Set.zero_mem_smul_iff {α : Type u_2} {β : Type u_1} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {s : Set α} {t : Set β} [inst : NoZeroSMulDivisors α β] :
theorem Set.zero_mem_smul_set_iff {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst : Zero β] [inst : SMulWithZero α β] {t : Set β} [inst : NoZeroSMulDivisors α β] {a : α} (ha : a 0) :
0 a t 0 t
theorem Set.pairwiseDisjoint_vadd_iff {α : Type u_1} [inst : AddLeftCancelSemigroup α] {s : Set α} {t : Set α} :
(Set.PairwiseDisjoint s fun x => x +ᵥ t) Set.InjOn (fun p => p.fst + p.snd) (s ×ˢ t)
theorem Set.pairwiseDisjoint_smul_iff {α : Type u_1} [inst : LeftCancelSemigroup α] {s : Set α} {t : Set α} :
(Set.PairwiseDisjoint s fun x => x t) Set.InjOn (fun p => p.fst * p.snd) (s ×ˢ t)
@[simp]
theorem Set.vadd_mem_vadd_set_iff {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {s : Set β} {a : α} {x : β} :
a +ᵥ x a +ᵥ s x s
@[simp]
theorem Set.smul_mem_smul_set_iff {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {s : Set β} {a : α} {x : β} :
a x a s x s
theorem Set.mem_vadd_set_iff_neg_vadd_mem {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {A : Set β} {a : α} {x : β} :
x a +ᵥ A -a +ᵥ x A
theorem Set.mem_smul_set_iff_inv_smul_mem {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {A : Set β} {a : α} {x : β} :
x a A a⁻¹ x A
theorem Set.mem_neg_vadd_set_iff {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {A : Set β} {a : α} {x : β} :
x -a +ᵥ A a +ᵥ x A
theorem Set.mem_inv_smul_set_iff {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {A : Set β} {a : α} {x : β} :
x a⁻¹ A a x A
theorem Set.preimage_vadd {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] (a : α) (t : Set β) :
(fun x => a +ᵥ x) ⁻¹' t = -a +ᵥ t
theorem Set.preimage_smul {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] (a : α) (t : Set β) :
(fun x => a x) ⁻¹' t = a⁻¹ t
theorem Set.preimage_vadd_neg {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] (a : α) (t : Set β) :
(fun x => -a +ᵥ x) ⁻¹' t = a +ᵥ t
theorem Set.preimage_smul_inv {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] (a : α) (t : Set β) :
(fun x => a⁻¹ x) ⁻¹' t = a t
@[simp]
theorem Set.set_vadd_subset_set_vadd_iff {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {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_1} [inst : Group α] [inst : MulAction α β] {A : Set β} {B : Set β} {a : α} :
a A a B A B
theorem Set.set_vadd_subset_iff {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {A : Set β} {B : Set β} {a : α} :
a +ᵥ A B A -a +ᵥ B
theorem Set.set_smul_subset_iff {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {A : Set β} {B : Set β} {a : α} :
a A B A a⁻¹ B
theorem Set.subset_set_vadd_iff {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {A : Set β} {B : Set β} {a : α} :
A a +ᵥ B -a +ᵥ A B
theorem Set.subset_set_smul_iff {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {A : Set β} {B : Set β} {a : α} :
A a B a⁻¹ A B
theorem Set.vadd_set_inter {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {s : Set β} {t : Set β} {a : α} :
a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
theorem Set.smul_set_inter {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {s : Set β} {t : Set β} {a : α} :
a (s t) = a s a t
theorem Set.vadd_set_sdiff {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {s : Set β} {t : Set β} {a : α} :
a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
theorem Set.smul_set_sdiff {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {s : Set β} {t : Set β} {a : α} :
a (s \ t) = a s \ a t
theorem Set.vadd_set_symm_diff {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {s : Set β} {t : Set β} {a : α} :
a +ᵥ s t = (a +ᵥ s) (a +ᵥ t)
theorem Set.smul_set_symm_diff {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {s : Set β} {t : Set β} {a : α} :
a s t = (a s) (a t)
@[simp]
theorem Set.vadd_set_univ {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {a : α} :
a +ᵥ Set.univ = Set.univ
@[simp]
theorem Set.smul_set_univ {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {a : α} :
a Set.univ = Set.univ
@[simp]
theorem Set.vadd_univ {α : Type u_1} {β : Type u_2} [inst : AddGroup α] [inst : AddAction α β] {s : Set α} (hs : Set.Nonempty s) :
s +ᵥ Set.univ = Set.univ
abbrev Set.vadd_univ.match_1 {α : Type u_1} {s : Set α} (motive : Set.Nonempty sProp) :
(hs : Set.Nonempty s) → ((a : α) → (ha : a s) → motive (_ : x, x s)) → motive hs
Equations
@[simp]
theorem Set.smul_univ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst : MulAction α β] {s : Set α} (hs : Set.Nonempty s) :
s Set.univ = Set.univ
theorem Set.vadd_inter_ne_empty_iff {α : Type u_1} [inst : AddGroup α] {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_1} [inst : Group α] {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_1} [inst : AddGroup α] {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_1} [inst : Group α] {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_1} [inst : AddGroup α] {s : Set α} {t : Set α} {x : αᵃᵒᵖ} :
(x +ᵥ s) t a b, (a s b t) -a + b = x.unop
theorem Set.op_smul_inter_ne_empty_iff {α : Type u_1} [inst : Group α] {s : Set α} {t : Set α} {x : αᵐᵒᵖ} :
x s t a b, (a s b t) a⁻¹ * b = x.unop
@[simp]
theorem Set.unionᵢ_neg_vadd {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {s : Set β} :
(Set.unionᵢ fun g => -g +ᵥ s) = Set.unionᵢ fun g => g +ᵥ s
@[simp]
theorem Set.unionᵢ_inv_smul {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {s : Set β} :
(Set.unionᵢ fun g => g⁻¹ s) = Set.unionᵢ fun g => g s
theorem Set.unionᵢ_vadd_eq_setOf_exists {α : Type u_2} {β : Type u_1} [inst : AddGroup α] [inst : AddAction α β] {s : Set β} :
(Set.unionᵢ fun g => g +ᵥ s) = { a | g, g +ᵥ a s }
theorem Set.unionᵢ_smul_eq_setOf_exists {α : Type u_2} {β : Type u_1} [inst : Group α] [inst : MulAction α β] {s : Set β} :
(Set.unionᵢ fun g => g s) = { a | g, g a s }
@[simp]
theorem Set.smul_mem_smul_set_iff₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) (A : Set β) (x : β) :
a x a A x A
theorem Set.mem_smul_set_iff_inv_smul_mem₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) (A : Set β) (x : β) :
x a A a⁻¹ x A
theorem Set.mem_inv_smul_set_iff₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) (A : Set β) (x : β) :
x a⁻¹ A a x A
theorem Set.preimage_smul₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) (t : Set β) :
(fun x => a x) ⁻¹' t = a⁻¹ t
theorem Set.preimage_smul_inv₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) (t : Set β) :
(fun x => a⁻¹ x) ⁻¹' t = a t
@[simp]
theorem Set.set_smul_subset_set_smul_iff₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
a A a B A B
theorem Set.set_smul_subset_iff₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
a A B A a⁻¹ B
theorem Set.subset_set_smul_iff₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) {A : Set β} {B : Set β} :
A a B a⁻¹ A B
theorem Set.smul_set_inter₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
a (s t) = a s a t
theorem Set.smul_set_sdiff₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
a (s \ t) = a s \ a t
theorem Set.smul_set_symm_diff₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {s : Set β} {t : Set β} {a : α} (ha : a 0) :
a s t = (a s) (a t)
theorem Set.smul_set_univ₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {a : α} (ha : a 0) :
a Set.univ = Set.univ
theorem Set.smul_univ₀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {s : Set α} (hs : ¬s 0) :
s Set.univ = Set.univ
theorem Set.smul_univ₀' {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst : MulAction α β] {s : Set α} (hs : Set.Nontrivial s) :
s Set.univ = Set.univ
@[simp]
theorem Set.smul_set_neg {α : Type u_2} {β : Type u_1} [inst : Monoid α] [inst : AddGroup β] [inst : DistribMulAction α β] (a : α) (t : Set β) :
a -t = -(a t)
@[simp]
theorem Set.smul_neg {α : Type u_2} {β : Type u_1} [inst : Monoid α] [inst : AddGroup β] [inst : DistribMulAction α β] (s : Set α) (t : Set β) :
s -t = -(s t)
@[simp]
theorem Set.neg_smul_set {α : Type u_2} {β : Type u_1} [inst : Ring α] [inst : AddCommGroup β] [inst : Module α β] (a : α) (t : Set β) :
-a t = -(a t)
@[simp]
theorem Set.neg_smul {α : Type u_2} {β : Type u_1} [inst : Ring α] [inst : AddCommGroup β] [inst : Module α β] (s : Set α) (t : Set β) :
-s t = -(s t)