Pointwise operations of sets

This file defines pointwise algebraic operations on sets.

Main declarations

For sets s and t and scalar a:

• s * t: Multiplication, set of all x * y where x ∈ s and y ∈ t.
• s + t: Addition, set of all x + y where x ∈ s and y ∈ t.
• s⁻¹: Inversion, set of all x⁻¹ where x ∈ s.
• -s: Negation, set of all -x where x ∈ s.
• s / t: Division, set of all x / y where x ∈ s and y ∈ t.
• s - t: Subtraction, set of all x - y where x ∈ s and y ∈ t.
• 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. As an unfortunate side effect, this means that n • s, where n : ℕ, is ambiguous between pointwise scaling and repeated pointwise addition; the former has (2 : ℕ) • {1, 2} = {2, 4}, while the latter has (2 : ℕ) • {1, 2} = {2, 3, 4}. See note [pointwise nat action].

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

Implementation notes

• The following expressions are considered in simp-normal form in a group: (fun h ↦ h * g) ⁻¹' s, (fun h ↦ g * h) ⁻¹' s, (fun h ↦ h * g⁻¹) ⁻¹' s, (fun h ↦ g⁻¹ * h) ⁻¹' s, s * t, s⁻¹, (1 : Set _) (and similarly for additive variants). Expressions equal to one of these will be simplified.
• 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.

Tags

set multiplication, set addition, pointwise addition, pointwise multiplication, pointwise subtraction

0/1 as sets

noncomputable def Set.zero {α : Type u_2} [Zero α] : Zero (Set α)

The set 0 : Set α is defined as {0} in locale Pointwise.

Equations

• Set.zero = { zero := {0} }

noncomputable def Set.one {α : Type u_2} [One α] : One (Set α)

The set 1 : Set α is defined as {1} in locale Pointwise.

Equations

• Set.one = { one := {1} }

theorem Set.singleton_zero {α : Type u_2} [Zero α] : {0} = 0

theorem Set.singleton_one {α : Type u_2} [One α] : {1} = 1

@[simp]

theorem Set.mem_zero {α : Type u_2} [Zero α] {a : α} : a ∈ 0 ↔ a = 0

@[simp]

theorem Set.mem_one {α : Type u_2} [One α] {a : α} : a ∈ 1 ↔ a = 1

theorem Set.zero_mem_zero {α : Type u_2} [Zero α] : 0 ∈ 0

theorem Set.one_mem_one {α : Type u_2} [One α] : 1 ∈ 1

@[simp]

theorem Set.zero_subset {α : Type u_2} [Zero α] {s : Set α} : 0 ⊆ s ↔ 0 ∈ s

@[simp]

theorem Set.one_subset {α : Type u_2} [One α] {s : Set α} : 1 ⊆ s ↔ 1 ∈ s

theorem Set.zero_nonempty {α : Type u_2} [Zero α] : Set.Nonempty 0

theorem Set.one_nonempty {α : Type u_2} [One α] : Set.Nonempty 1

@[simp]

theorem Set.image_zero {α : Type u_2} {β : Type u_3} [Zero α] {f : α → β} : f '' 0 = {f 0}

@[simp]

theorem Set.image_one {α : Type u_2} {β : Type u_3} [One α] {f : α → β} : f '' 1 = {f 1}

theorem Set.subset_zero_iff_eq {α : Type u_2} [Zero α] {s : Set α} : s ⊆ 0 ↔ s = ∅ ∨ s = 0

theorem Set.subset_one_iff_eq {α : Type u_2} [One α] {s : Set α} : s ⊆ 1 ↔ s = ∅ ∨ s = 1

theorem Set.Nonempty.subset_zero_iff {α : Type u_2} [Zero α] {s : Set α} (h : s.Nonempty) : s ⊆ 0 ↔ s = 0

theorem Set.Nonempty.subset_one_iff {α : Type u_2} [One α] {s : Set α} (h : s.Nonempty) : s ⊆ 1 ↔ s = 1

noncomputable def Set.singletonZeroHom {α : Type u_2} [Zero α] : ZeroHom α (Set α)

The singleton operation as a ZeroHom.

Equations

• Set.singletonZeroHom = { toFun := singleton, map_zero' := ⋯ }

noncomputable def Set.singletonOneHom {α : Type u_2} [One α] : OneHom α (Set α)

The singleton operation as a OneHom.

Equations

• Set.singletonOneHom = { toFun := singleton, map_one' := ⋯ }

@[simp]

theorem Set.coe_singletonZeroHom {α : Type u_2} [Zero α] : ⇑Set.singletonZeroHom = singleton

@[simp]

theorem Set.coe_singletonOneHom {α : Type u_2} [One α] : ⇑Set.singletonOneHom = singleton

Set negation/inversion

def Set.neg {α : Type u_2} [Neg α] : Neg (Set α)

The pointwise negation of set -s is defined as {x | -x ∈ s} in locale Pointwise. It is equal to {-x | x ∈ s}, see Set.image_neg.

Equations

• Set.neg = { neg := Set.preimage Neg.neg }

def Set.inv {α : Type u_2} [Inv α] : Inv (Set α)

The pointwise inversion of set s⁻¹ is defined as {x | x⁻¹ ∈ s} in locale Pointwise. It is equal to {x⁻¹ | x ∈ s}, see Set.image_inv.

Equations

• Set.inv = { inv := Set.preimage Inv.inv }

@[simp]

theorem Set.mem_neg {α : Type u_2} [Neg α] {s : Set α} {a : α} : a ∈ -s ↔ -a ∈ s

@[simp]

theorem Set.mem_inv {α : Type u_2} [Inv α] {s : Set α} {a : α} : a ∈ s⁻¹ ↔ a⁻¹ ∈ s

@[simp]

theorem Set.neg_preimage {α : Type u_2} [Neg α] {s : Set α} : Neg.neg ⁻¹' s = -s

@[simp]

theorem Set.inv_preimage {α : Type u_2} [Inv α] {s : Set α} : Inv.inv ⁻¹' s = s⁻¹

@[simp]

theorem Set.neg_empty {α : Type u_2} [Neg α] : -∅ = ∅

@[simp]

theorem Set.inv_empty {α : Type u_2} [Inv α] : ∅⁻¹ = ∅

@[simp]

theorem Set.neg_univ {α : Type u_2} [Neg α] : -Set.univ = Set.univ

@[simp]

theorem Set.inv_univ {α : Type u_2} [Inv α] : Set.univ⁻¹ = Set.univ

@[simp]

theorem Set.inter_neg {α : Type u_2} [Neg α] {s : Set α} {t : Set α} : -(s ∩ t) = -s ∩ -t

@[simp]

theorem Set.inter_inv {α : Type u_2} [Inv α] {s : Set α} {t : Set α} : (s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹

@[simp]

theorem Set.union_neg {α : Type u_2} [Neg α] {s : Set α} {t : Set α} : -(s ∪ t) = -s ∪ -t

@[simp]

theorem Set.union_inv {α : Type u_2} [Inv α] {s : Set α} {t : Set α} : (s ∪ t)⁻¹ = s⁻¹ ∪ t⁻¹

@[simp]

theorem Set.iInter_neg {α : Type u_2} {ι : Sort u_5} [Neg α] (s : ι → Set α) : -⋂ (i : ι), s i = ⋂ (i : ι), -s i

@[simp]

theorem Set.iInter_inv {α : Type u_2} {ι : Sort u_5} [Inv α] (s : ι → Set α) : (⋂ (i : ι), s i)⁻¹ = ⋂ (i : ι), (s i)⁻¹

@[simp]

theorem Set.iUnion_neg {α : Type u_2} {ι : Sort u_5} [Neg α] (s : ι → Set α) : -⋃ (i : ι), s i = ⋃ (i : ι), -s i

@[simp]

theorem Set.iUnion_inv {α : Type u_2} {ι : Sort u_5} [Inv α] (s : ι → Set α) : (⋃ (i : ι), s i)⁻¹ = ⋃ (i : ι), (s i)⁻¹

@[simp]

theorem Set.compl_neg {α : Type u_2} [Neg α] {s : Set α} : -sᶜ = (-s)ᶜ

@[simp]

theorem Set.compl_inv {α : Type u_2} [Inv α] {s : Set α} : sᶜ⁻¹ = s⁻¹ᶜ

theorem Set.neg_mem_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} {a : α} : -a ∈ -s ↔ a ∈ s

theorem Set.inv_mem_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} {a : α} : a⁻¹ ∈ s⁻¹ ↔ a ∈ s

@[simp]

theorem Set.nonempty_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} : (-s).Nonempty ↔ s.Nonempty

@[simp]

theorem Set.nonempty_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} : s⁻¹.Nonempty ↔ s.Nonempty

theorem Set.Nonempty.neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} (h : s.Nonempty) : (-s).Nonempty

theorem Set.Nonempty.inv {α : Type u_2} [InvolutiveInv α] {s : Set α} (h : s.Nonempty) : s⁻¹.Nonempty

@[simp]

theorem Set.image_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} : Neg.neg '' s = -s

@[simp]

theorem Set.image_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} : Inv.inv '' s = s⁻¹

@[simp]

theorem Set.neg_eq_empty {α : Type u_2} [InvolutiveNeg α] {s : Set α} : -s = ∅ ↔ s = ∅

@[simp]

theorem Set.inv_eq_empty {α : Type u_2} [InvolutiveInv α] {s : Set α} : s⁻¹ = ∅ ↔ s = ∅

theorem Set.involutiveNeg.proof_1 {α : Type u_1} [InvolutiveNeg α] (s : Set α) : (fun (x : α) => - -x) ⁻¹' s = s

noncomputable instance Set.involutiveNeg {α : Type u_2} [InvolutiveNeg α] : InvolutiveNeg (Set α)

Equations

• Set.involutiveNeg = InvolutiveNeg.mk ⋯

noncomputable instance Set.involutiveInv {α : Type u_2} [InvolutiveInv α] : InvolutiveInv (Set α)

Equations

• Set.involutiveInv = InvolutiveInv.mk ⋯

@[simp]

theorem Set.neg_subset_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} {t : Set α} : -s ⊆ -t ↔ s ⊆ t

@[simp]

theorem Set.inv_subset_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} {t : Set α} : s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t

theorem Set.neg_subset {α : Type u_2} [InvolutiveNeg α] {s : Set α} {t : Set α} : -s ⊆ t ↔ s ⊆ -t

theorem Set.inv_subset {α : Type u_2} [InvolutiveInv α] {s : Set α} {t : Set α} : s⁻¹ ⊆ t ↔ s ⊆ t⁻¹

@[simp]

theorem Set.neg_singleton {α : Type u_2} [InvolutiveNeg α] (a : α) : -{a} = {-a}

@[simp]

theorem Set.inv_singleton {α : Type u_2} [InvolutiveInv α] (a : α) : {a}⁻¹ = {a⁻¹}

@[simp]

theorem Set.neg_insert {α : Type u_2} [InvolutiveNeg α] (a : α) (s : Set α) : -insert a s = insert (-a) (-s)

@[simp]

theorem Set.inv_insert {α : Type u_2} [InvolutiveInv α] (a : α) (s : Set α) : (insert a s)⁻¹ = insert a⁻¹ s⁻¹

theorem Set.neg_range {α : Type u_2} [InvolutiveNeg α] {ι : Sort u_5} {f : ι → α} : -Set.range f = Set.range fun (i : ι) => -f i

theorem Set.inv_range {α : Type u_2} [InvolutiveInv α] {ι : Sort u_5} {f : ι → α} : (Set.range f)⁻¹ = Set.range fun (i : ι) => (f i)⁻¹

theorem Set.image_op_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} : AddOpposite.op '' (-s) = -AddOpposite.op '' s

theorem Set.image_op_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} : MulOpposite.op '' s⁻¹ = (MulOpposite.op '' s)⁻¹

Set addition/multiplication

def Set.add {α : Type u_2} [Add α] : Add (Set α)

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

Equations

• Set.add = { add := Set.image2 fun (x1 x2 : α) => x1 + x2 }

def Set.mul {α : Type u_2} [Mul α] : Mul (Set α)

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

Equations

• Set.mul = { mul := Set.image2 fun (x1 x2 : α) => x1 * x2 }

@[simp]

theorem Set.image2_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} : Set.image2 (fun (x1 x2 : α) => x1 + x2) s t = s + t

@[simp]

theorem Set.image2_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : Set.image2 (fun (x1 x2 : α) => x1 * x2) s t = s * t

theorem Set.mem_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} {a : α} : a ∈ s + t ↔ ∃ x ∈ s, ∃ y ∈ t, x + y = a

theorem Set.mem_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {a : α} : a ∈ s * t ↔ ∃ x ∈ s, ∃ y ∈ t, x * y = a

theorem Set.add_mem_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} {a : α} {b : α} : a ∈ s → b ∈ t → a + b ∈ s + t

theorem Set.mul_mem_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {a : α} {b : α} : a ∈ s → b ∈ t → a * b ∈ s * t

theorem Set.add_image_prod {α : Type u_2} [Add α] {s : Set α} {t : Set α} : (fun (x : α × α) => x.1 + x.2) '' s ×ˢ t = s + t

theorem Set.image_mul_prod {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : (fun (x : α × α) => x.1 * x.2) '' s ×ˢ t = s * t

@[simp]

theorem Set.empty_add {α : Type u_2} [Add α] {s : Set α} : ∅ + s = ∅

@[simp]

theorem Set.empty_mul {α : Type u_2} [Mul α] {s : Set α} : ∅ * s = ∅

@[simp]

theorem Set.add_empty {α : Type u_2} [Add α] {s : Set α} : s + ∅ = ∅

@[simp]

theorem Set.mul_empty {α : Type u_2} [Mul α] {s : Set α} : s * ∅ = ∅

@[simp]

theorem Set.add_eq_empty {α : Type u_2} [Add α] {s : Set α} {t : Set α} : s + t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.mul_eq_empty {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : s * t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.add_nonempty {α : Type u_2} [Add α] {s : Set α} {t : Set α} : (s + t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Set.mul_nonempty {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : (s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Set.Nonempty.add {α : Type u_2} [Add α] {s : Set α} {t : Set α} : s.Nonempty → t.Nonempty → (s + t).Nonempty

theorem Set.Nonempty.mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : s.Nonempty → t.Nonempty → (s * t).Nonempty

theorem Set.Nonempty.of_add_left {α : Type u_2} [Add α] {s : Set α} {t : Set α} : (s + t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_mul_left {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : (s * t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_add_right {α : Type u_2} [Add α] {s : Set α} {t : Set α} : (s + t).Nonempty → t.Nonempty

theorem Set.Nonempty.of_mul_right {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : (s * t).Nonempty → t.Nonempty

@[simp]

theorem Set.add_singleton {α : Type u_2} [Add α] {s : Set α} {b : α} : s + {b} = (fun (x : α) => x + b) '' s

@[simp]

theorem Set.mul_singleton {α : Type u_2} [Mul α] {s : Set α} {b : α} : s * {b} = (fun (x : α) => x * b) '' s

@[simp]

theorem Set.singleton_add {α : Type u_2} [Add α] {t : Set α} {a : α} : {a} + t = (fun (x : α) => a + x) '' t

@[simp]

theorem Set.singleton_mul {α : Type u_2} [Mul α] {t : Set α} {a : α} : {a} * t = (fun (x : α) => a * x) '' t

theorem Set.singleton_add_singleton {α : Type u_2} [Add α] {a : α} {b : α} : {a} + {b} = {a + b}

theorem Set.singleton_mul_singleton {α : Type u_2} [Mul α] {a : α} {b : α} : {a} * {b} = {a * b}

theorem Set.add_subset_add {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ + s₂ ⊆ t₁ + t₂

theorem Set.mul_subset_mul {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ * s₂ ⊆ t₁ * t₂

theorem Set.add_subset_add_left {α : Type u_2} [Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂

theorem Set.mul_subset_mul_left {α : Type u_2} [Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂

theorem Set.add_subset_add_right {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t

theorem Set.mul_subset_mul_right {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t

theorem Set.add_subset_iff {α : Type u_2} [Add α] {s : Set α} {t : Set α} {u : Set α} : s + t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ u

theorem Set.mul_subset_iff {α : Type u_2} [Mul α] {s : Set α} {t : Set α} {u : Set α} : s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u

theorem Set.union_add {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)

theorem Set.union_mul {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : (s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t

theorem Set.add_union {α : Type u_2} [Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)

theorem Set.mul_union {α : Type u_2} [Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂

theorem Set.inter_add_subset {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)

theorem Set.inter_mul_subset {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)

theorem Set.add_inter_subset {α : Type u_2} [Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)

theorem Set.mul_inter_subset {α : Type u_2} [Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)

theorem Set.inter_add_union_subset_union {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)

theorem Set.inter_mul_union_subset_union {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂

theorem Set.union_add_inter_subset_union {α : Type u_2} [Add α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)

theorem Set.union_mul_inter_subset_union {α : Type u_2} [Mul α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂

theorem Set.iUnion_add_left_image {α : Type u_2} [Add α] {s : Set α} {t : Set α} : ⋃ a ∈ s, (fun (x : α) => a + x) '' t = s + t

theorem Set.iUnion_mul_left_image {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : ⋃ a ∈ s, (fun (x : α) => a * x) '' t = s * t

theorem Set.iUnion_add_right_image {α : Type u_2} [Add α] {s : Set α} {t : Set α} : ⋃ a ∈ t, (fun (x : α) => x + a) '' s = s + t

theorem Set.iUnion_mul_right_image {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : ⋃ a ∈ t, (fun (x : α) => x * a) '' s = s * t

theorem Set.iUnion_add {α : Type u_2} {ι : Sort u_5} [Add α] (s : ι → Set α) (t : Set α) : (⋃ (i : ι), s i) + t = ⋃ (i : ι), s i + t

theorem Set.iUnion_mul {α : Type u_2} {ι : Sort u_5} [Mul α] (s : ι → Set α) (t : Set α) : (⋃ (i : ι), s i) * t = ⋃ (i : ι), s i * t

theorem Set.add_iUnion {α : Type u_2} {ι : Sort u_5} [Add α] (s : Set α) (t : ι → Set α) : s + ⋃ (i : ι), t i = ⋃ (i : ι), s + t i

theorem Set.mul_iUnion {α : Type u_2} {ι : Sort u_5} [Mul α] (s : Set α) (t : ι → Set α) : s * ⋃ (i : ι), t i = ⋃ (i : ι), s * t i

theorem Set.iUnion₂_add {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Add α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋃ (i : ι), ⋃ (j : κ i), s i j) + t = ⋃ (i : ι), ⋃ (j : κ i), s i j + t

theorem Set.iUnion₂_mul {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Mul α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋃ (i : ι), ⋃ (j : κ i), s i j) * t = ⋃ (i : ι), ⋃ (j : κ i), s i j * t

theorem Set.add_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Add α] (s : Set α) (t : (i : ι) → κ i → Set α) : s + ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s + t i j

theorem Set.mul_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Mul α] (s : Set α) (t : (i : ι) → κ i → Set α) : s * ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s * t i j

theorem Set.iInter_add_subset {α : Type u_2} {ι : Sort u_5} [Add α] (s : ι → Set α) (t : Set α) : (⋂ (i : ι), s i) + t ⊆ ⋂ (i : ι), s i + t

theorem Set.iInter_mul_subset {α : Type u_2} {ι : Sort u_5} [Mul α] (s : ι → Set α) (t : Set α) : (⋂ (i : ι), s i) * t ⊆ ⋂ (i : ι), s i * t

theorem Set.add_iInter_subset {α : Type u_2} {ι : Sort u_5} [Add α] (s : Set α) (t : ι → Set α) : s + ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s + t i

theorem Set.mul_iInter_subset {α : Type u_2} {ι : Sort u_5} [Mul α] (s : Set α) (t : ι → Set α) : s * ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s * t i

theorem Set.iInter₂_add_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Add α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋂ (i : ι), ⋂ (j : κ i), s i j) + t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j + t

theorem Set.iInter₂_mul_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Mul α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋂ (i : ι), ⋂ (j : κ i), s i j) * t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j * t

theorem Set.add_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Add α] (s : Set α) (t : (i : ι) → κ i → Set α) : s + ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s + t i j

theorem Set.mul_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Mul α] (s : Set α) (t : (i : ι) → κ i → Set α) : s * ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s * t i j

theorem Set.singletonAddHom.proof_1 {α : Type u_1} [Add α] : ∀ (x x_1 : α), {x + x_1} = {x} + {x_1}

noncomputable def Set.singletonAddHom {α : Type u_2} [Add α] : AddHom α (Set α)

The singleton operation as an AddHom.

Equations

• Set.singletonAddHom = { toFun := singleton, map_add' := ⋯ }

noncomputable def Set.singletonMulHom {α : Type u_2} [Mul α] : α →ₙ* Set α

The singleton operation as a MulHom.

Equations

• Set.singletonMulHom = { toFun := singleton, map_mul' := ⋯ }

@[simp]

theorem Set.coe_singletonAddHom {α : Type u_2} [Add α] : ⇑Set.singletonAddHom = singleton

@[simp]

theorem Set.coe_singletonMulHom {α : Type u_2} [Mul α] : ⇑Set.singletonMulHom = singleton

@[simp]

theorem Set.singletonAddHom_apply {α : Type u_2} [Add α] (a : α) : Set.singletonAddHom a = {a}

@[simp]

theorem Set.singletonMulHom_apply {α : Type u_2} [Mul α] (a : α) : Set.singletonMulHom a = {a}

@[simp]

theorem Set.image_op_add {α : Type u_2} [Add α] {s : Set α} {t : Set α} : AddOpposite.op '' (s + t) = AddOpposite.op '' t + AddOpposite.op '' s

@[simp]

theorem Set.image_op_mul {α : Type u_2} [Mul α] {s : Set α} {t : Set α} : MulOpposite.op '' (s * t) = MulOpposite.op '' t * MulOpposite.op '' s

Set subtraction/division

def Set.sub {α : Type u_2} [Sub α] : Sub (Set α)

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

Equations

• Set.sub = { sub := Set.image2 fun (x1 x2 : α) => x1 - x2 }

def Set.div {α : Type u_2} [Div α] : Div (Set α)

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

Equations

• Set.div = { div := Set.image2 fun (x1 x2 : α) => x1 / x2 }

@[simp]

theorem Set.image2_sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : Set.image2 Sub.sub s t = s - t

@[simp]

theorem Set.image2_div {α : Type u_2} [Div α] {s : Set α} {t : Set α} : Set.image2 Div.div s t = s / t

theorem Set.mem_sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} {a : α} : a ∈ s - t ↔ ∃ x ∈ s, ∃ y ∈ t, x - y = a

theorem Set.mem_div {α : Type u_2} [Div α] {s : Set α} {t : Set α} {a : α} : a ∈ s / t ↔ ∃ x ∈ s, ∃ y ∈ t, x / y = a

theorem Set.sub_mem_sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} {a : α} {b : α} : a ∈ s → b ∈ t → a - b ∈ s - t

theorem Set.div_mem_div {α : Type u_2} [Div α] {s : Set α} {t : Set α} {a : α} {b : α} : a ∈ s → b ∈ t → a / b ∈ s / t

theorem Set.sub_image_prod {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : (fun (x : α × α) => x.1 - x.2) '' s ×ˢ t = s - t

theorem Set.image_div_prod {α : Type u_2} [Div α] {s : Set α} {t : Set α} : (fun (x : α × α) => x.1 / x.2) '' s ×ˢ t = s / t

@[simp]

theorem Set.empty_sub {α : Type u_2} [Sub α] {s : Set α} : ∅ - s = ∅

@[simp]

theorem Set.empty_div {α : Type u_2} [Div α] {s : Set α} : ∅ / s = ∅

@[simp]

theorem Set.sub_empty {α : Type u_2} [Sub α] {s : Set α} : s - ∅ = ∅

@[simp]

theorem Set.div_empty {α : Type u_2} [Div α] {s : Set α} : s / ∅ = ∅

@[simp]

theorem Set.sub_eq_empty {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : s - t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.div_eq_empty {α : Type u_2} [Div α] {s : Set α} {t : Set α} : s / t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.sub_nonempty {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : (s - t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Set.div_nonempty {α : Type u_2} [Div α] {s : Set α} {t : Set α} : (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Set.Nonempty.sub {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : s.Nonempty → t.Nonempty → (s - t).Nonempty

theorem Set.Nonempty.div {α : Type u_2} [Div α] {s : Set α} {t : Set α} : s.Nonempty → t.Nonempty → (s / t).Nonempty

theorem Set.Nonempty.of_sub_left {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : (s - t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_div_left {α : Type u_2} [Div α] {s : Set α} {t : Set α} : (s / t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_sub_right {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : (s - t).Nonempty → t.Nonempty

theorem Set.Nonempty.of_div_right {α : Type u_2} [Div α] {s : Set α} {t : Set α} : (s / t).Nonempty → t.Nonempty

@[simp]

theorem Set.sub_singleton {α : Type u_2} [Sub α] {s : Set α} {b : α} : s - {b} = (fun (x : α) => x - b) '' s

@[simp]

theorem Set.div_singleton {α : Type u_2} [Div α] {s : Set α} {b : α} : s / {b} = (fun (x : α) => x / b) '' s

@[simp]

theorem Set.singleton_sub {α : Type u_2} [Sub α] {t : Set α} {a : α} : {a} - t = (fun (x1 x2 : α) => x1 - x2) a '' t

@[simp]

theorem Set.singleton_div {α : Type u_2} [Div α] {t : Set α} {a : α} : {a} / t = (fun (x1 x2 : α) => x1 / x2) a '' t

theorem Set.singleton_sub_singleton {α : Type u_2} [Sub α] {a : α} {b : α} : {a} - {b} = {a - b}

theorem Set.singleton_div_singleton {α : Type u_2} [Div α] {a : α} {b : α} : {a} / {b} = {a / b}

theorem Set.sub_subset_sub {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ - s₂ ⊆ t₁ - t₂

theorem Set.div_subset_div {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ / s₂ ⊆ t₁ / t₂

theorem Set.sub_subset_sub_left {α : Type u_2} [Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂

theorem Set.div_subset_div_left {α : Type u_2} [Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂

theorem Set.sub_subset_sub_right {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t

theorem Set.div_subset_div_right {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t

theorem Set.sub_subset_iff {α : Type u_2} [Sub α] {s : Set α} {t : Set α} {u : Set α} : s - t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x - y ∈ u

theorem Set.div_subset_iff {α : Type u_2} [Div α] {s : Set α} {t : Set α} {u : Set α} : s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u

theorem Set.union_sub {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)

theorem Set.union_div {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t

theorem Set.sub_union {α : Type u_2} [Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)

theorem Set.div_union {α : Type u_2} [Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂

theorem Set.inter_sub_subset {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)

theorem Set.inter_div_subset {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} : s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)

theorem Set.sub_inter_subset {α : Type u_2} [Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)

theorem Set.div_inter_subset {α : Type u_2} [Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} : s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)

theorem Set.inter_sub_union_subset_union {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)

theorem Set.inter_div_union_subset_union {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

theorem Set.union_sub_inter_subset_union {α : Type u_2} [Sub α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)

theorem Set.union_div_inter_subset_union {α : Type u_2} [Div α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂

theorem Set.iUnion_sub_left_image {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : ⋃ a ∈ s, (fun (x : α) => a - x) '' t = s - t

theorem Set.iUnion_div_left_image {α : Type u_2} [Div α] {s : Set α} {t : Set α} : ⋃ a ∈ s, (fun (x : α) => a / x) '' t = s / t

theorem Set.iUnion_sub_right_image {α : Type u_2} [Sub α] {s : Set α} {t : Set α} : ⋃ a ∈ t, (fun (x : α) => x - a) '' s = s - t

theorem Set.iUnion_div_right_image {α : Type u_2} [Div α] {s : Set α} {t : Set α} : ⋃ a ∈ t, (fun (x : α) => x / a) '' s = s / t

theorem Set.iUnion_sub {α : Type u_2} {ι : Sort u_5} [Sub α] (s : ι → Set α) (t : Set α) : (⋃ (i : ι), s i) - t = ⋃ (i : ι), s i - t

theorem Set.iUnion_div {α : Type u_2} {ι : Sort u_5} [Div α] (s : ι → Set α) (t : Set α) : (⋃ (i : ι), s i) / t = ⋃ (i : ι), s i / t

theorem Set.sub_iUnion {α : Type u_2} {ι : Sort u_5} [Sub α] (s : Set α) (t : ι → Set α) : s - ⋃ (i : ι), t i = ⋃ (i : ι), s - t i

theorem Set.div_iUnion {α : Type u_2} {ι : Sort u_5} [Div α] (s : Set α) (t : ι → Set α) : s / ⋃ (i : ι), t i = ⋃ (i : ι), s / t i

theorem Set.iUnion₂_sub {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Sub α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋃ (i : ι), ⋃ (j : κ i), s i j) - t = ⋃ (i : ι), ⋃ (j : κ i), s i j - t

theorem Set.iUnion₂_div {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Div α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋃ (i : ι), ⋃ (j : κ i), s i j) / t = ⋃ (i : ι), ⋃ (j : κ i), s i j / t

theorem Set.sub_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Sub α] (s : Set α) (t : (i : ι) → κ i → Set α) : s - ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s - t i j

theorem Set.div_iUnion₂ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Div α] (s : Set α) (t : (i : ι) → κ i → Set α) : s / ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s / t i j

theorem Set.iInter_sub_subset {α : Type u_2} {ι : Sort u_5} [Sub α] (s : ι → Set α) (t : Set α) : (⋂ (i : ι), s i) - t ⊆ ⋂ (i : ι), s i - t

theorem Set.iInter_div_subset {α : Type u_2} {ι : Sort u_5} [Div α] (s : ι → Set α) (t : Set α) : (⋂ (i : ι), s i) / t ⊆ ⋂ (i : ι), s i / t

theorem Set.sub_iInter_subset {α : Type u_2} {ι : Sort u_5} [Sub α] (s : Set α) (t : ι → Set α) : s - ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s - t i

theorem Set.div_iInter_subset {α : Type u_2} {ι : Sort u_5} [Div α] (s : Set α) (t : ι → Set α) : s / ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s / t i

theorem Set.iInter₂_sub_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Sub α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋂ (i : ι), ⋂ (j : κ i), s i j) - t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j - t

theorem Set.iInter₂_div_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Div α] (s : (i : ι) → κ i → Set α) (t : Set α) : (⋂ (i : ι), ⋂ (j : κ i), s i j) / t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j / t

theorem Set.sub_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Sub α] (s : Set α) (t : (i : ι) → κ i → Set α) : s - ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s - t i j

theorem Set.div_iInter₂_subset {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [Div α] (s : Set α) (t : (i : ι) → κ i → Set α) : s / ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s / t i j

Translation/scaling of sets

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

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

Equations

• Set.vaddSet = { vadd := fun (a : α) => Set.image fun (x : β) => a +ᵥ x }

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

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

Equations

• Set.smulSet = { smul := fun (a : α) => Set.image fun (x : β) => a • x }

def Set.vadd {α : Type u_2} {β : Type u_3} [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

• Set.vadd = { vadd := Set.image2 fun (x1 : α) (x2 : β) => x1 +ᵥ x2 }

def Set.smul {α : Type u_2} {β : Type u_3} [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

• Set.smul = { smul := Set.image2 fun (x1 : α) (x2 : β) => x1 • x2 }

@[simp]

theorem Set.image2_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : Set.image2 VAdd.vadd s t = s +ᵥ t

@[simp]

theorem Set.image2_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : Set.image2 SMul.smul s t = s • t

theorem Set.vadd_image_prod {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (fun (x : α × β) => x.1 +ᵥ x.2) '' s ×ˢ t = s +ᵥ t

theorem Set.image_smul_prod {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (fun (x : α × β) => x.1 • x.2) '' s ×ˢ t = s • t

theorem Set.mem_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {b : β} : b ∈ s +ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x +ᵥ y = b

theorem Set.mem_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {b : β} : b ∈ s • t ↔ ∃ x ∈ s, ∃ y ∈ t, x • y = b

theorem Set.vadd_mem_vadd {α : Type u_2} {β : Type u_3} [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} [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} [VAdd α β] {t : Set β} : ∅ +ᵥ t = ∅

@[simp]

theorem Set.empty_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} : ∅ • t = ∅

@[simp]

theorem Set.vadd_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} : s +ᵥ ∅ = ∅

@[simp]

theorem Set.smul_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} : s • ∅ = ∅

@[simp]

theorem Set.vadd_eq_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.smul_eq_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : s • t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.vadd_nonempty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (s +ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[simp]

theorem Set.smul_nonempty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Set.Nonempty.vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : s.Nonempty → t.Nonempty → (s +ᵥ t).Nonempty

theorem Set.Nonempty.smul {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : s.Nonempty → t.Nonempty → (s • t).Nonempty

theorem Set.Nonempty.of_vadd_left {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (s +ᵥ t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (s • t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (s +ᵥ t).Nonempty → t.Nonempty

theorem Set.Nonempty.of_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (s • t).Nonempty → t.Nonempty

@[simp]

theorem Set.vadd_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {b : β} : s +ᵥ {b} = (fun (x : α) => x +ᵥ b) '' s

@[simp]

theorem Set.smul_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {b : β} : s • {b} = (fun (x : α) => x • b) '' s

@[simp]

theorem Set.singleton_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} : {a} +ᵥ t = a +ᵥ t

@[simp]

theorem Set.singleton_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} : {a} • t = a • t

@[simp]

theorem Set.singleton_vadd_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} : {a} +ᵥ {b} = {a +ᵥ b}

@[simp]

theorem Set.singleton_smul_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} : {a} • {b} = {a • b}

theorem Set.vadd_subset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂

theorem Set.smul_subset_smul {α : Type u_2} {β : Type u_3} [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_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂

theorem Set.smul_subset_smul_left {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂

theorem Set.vadd_subset_vadd_right {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t

theorem Set.smul_subset_smul_right {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t

theorem Set.vadd_subset_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} {u : Set β} : s +ᵥ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a +ᵥ b ∈ u

theorem Set.smul_subset_iff {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} {u : Set β} : s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u

theorem Set.union_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : s₁ ∪ s₂ +ᵥ t = s₁ +ᵥ t ∪ (s₂ +ᵥ t)

theorem Set.union_smul {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : (s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t

theorem Set.vadd_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : s +ᵥ (t₁ ∪ t₂) = s +ᵥ t₁ ∪ (s +ᵥ t₂)

theorem Set.smul_union {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂

theorem Set.inter_vadd_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)

theorem Set.inter_smul_subset {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t : Set β} : (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t

theorem Set.vadd_inter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : s +ᵥ t₁ ∩ t₂ ⊆ (s +ᵥ t₁) ∩ (s +ᵥ t₂)

theorem Set.smul_inter_subset {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t₁ : Set β} {t₂ : Set β} : s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂

theorem Set.inter_vadd_union_subset_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : s₁ ∩ s₂ +ᵥ (t₁ ∪ t₂) ⊆ s₁ +ᵥ t₁ ∪ (s₂ +ᵥ t₂)

theorem Set.inter_smul_union_subset_union {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : (s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂

theorem Set.union_vadd_inter_subset_union {α : Type u_2} {β : Type u_3} [VAdd α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : s₁ ∪ s₂ +ᵥ t₁ ∩ t₂ ⊆ s₁ +ᵥ t₁ ∪ (s₂ +ᵥ t₂)

theorem Set.union_smul_inter_subset_union {α : Type u_2} {β : Type u_3} [SMul α β] {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} : (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂

theorem Set.iUnion_vadd_left_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : ⋃ a ∈ s, a +ᵥ t = s +ᵥ t

theorem Set.iUnion_smul_left_image {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : ⋃ a ∈ s, a • t = s • t

theorem Set.iUnion_vadd_right_image {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : ⋃ a ∈ t, (fun (x : α) => x +ᵥ a) '' s = s +ᵥ t

theorem Set.iUnion_smul_right_image {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : ⋃ a ∈ t, (fun (x : α) => x • a) '' s = s • t

theorem Set.iUnion_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : ι → Set α) (t : Set β) : (⋃ (i : ι), s i) +ᵥ t = ⋃ (i : ι), s i +ᵥ t

theorem Set.iUnion_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : ι → Set α) (t : Set β) : (⋃ (i : ι), s i) • t = ⋃ (i : ι), s i • t

theorem Set.vadd_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : Set α) (t : ι → Set β) : s +ᵥ ⋃ (i : ι), t i = ⋃ (i : ι), s +ᵥ t i

theorem Set.smul_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : Set α) (t : ι → Set β) : s • ⋃ (i : ι), t i = ⋃ (i : ι), s • t i

theorem Set.iUnion₂_vadd {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (s : (i : ι) → κ i → Set α) (t : Set β) : (⋃ (i : ι), ⋃ (j : κ i), s i j) +ᵥ t = ⋃ (i : ι), ⋃ (j : κ i), s i j +ᵥ t

theorem Set.iUnion₂_smul {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (s : (i : ι) → κ i → Set α) (t : Set β) : (⋃ (i : ι), ⋃ (j : κ i), s i j) • t = ⋃ (i : ι), ⋃ (j : κ i), s i j • t

theorem Set.vadd_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (s : Set α) (t : (i : ι) → κ i → Set β) : s +ᵥ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s +ᵥ t i j

theorem Set.smul_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (s : Set α) (t : (i : ι) → κ i → Set β) : s • ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s • t i j

theorem Set.iInter_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : ι → Set α) (t : Set β) : (⋂ (i : ι), s i) +ᵥ t ⊆ ⋂ (i : ι), s i +ᵥ t

theorem Set.iInter_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : ι → Set α) (t : Set β) : (⋂ (i : ι), s i) • t ⊆ ⋂ (i : ι), s i • t

theorem Set.vadd_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (s : Set α) (t : ι → Set β) : s +ᵥ ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s +ᵥ t i

theorem Set.smul_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (s : Set α) (t : ι → Set β) : s • ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s • t i

theorem Set.iInter₂_vadd_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (s : (i : ι) → κ i → Set α) (t : Set β) : (⋂ (i : ι), ⋂ (j : κ i), s i j) +ᵥ t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j +ᵥ t

theorem Set.iInter₂_smul_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (s : (i : ι) → κ i → Set α) (t : Set β) : (⋂ (i : ι), ⋂ (j : κ i), s i j) • t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j • t

theorem Set.vadd_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (s : Set α) (t : (i : ι) → κ i → Set β) : s +ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s +ᵥ t i j

theorem Set.smul_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (s : Set α) (t : (i : ι) → κ i → Set β) : s • ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s • t i j

theorem Set.vadd_set_subset_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} {s : Set α} : a ∈ s → a +ᵥ t ⊆ s +ᵥ t

theorem Set.smul_set_subset_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} {s : Set α} : a ∈ s → a • t ⊆ s • t

@[simp]

theorem Set.iUnion_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] (s : Set α) (t : Set β) : ⋃ a ∈ s, a +ᵥ t = s +ᵥ t

@[simp]

theorem Set.iUnion_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] (s : Set α) (t : Set β) : ⋃ a ∈ s, a • t = s • t

theorem Set.image_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} : (fun (x : β) => a +ᵥ x) '' t = a +ᵥ t

theorem Set.image_smul {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} : (fun (x : β) => a • x) '' t = a • t

theorem Set.mem_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {t : Set β} {a : α} {x : β} : x ∈ a +ᵥ t ↔ ∃ y ∈ t, a +ᵥ y = x

theorem Set.mem_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {t : Set β} {a : α} {x : β} : x ∈ a • t ↔ ∃ y ∈ t, a • y = x

theorem Set.vadd_mem_vadd_set {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} {b : β} : b ∈ s → a +ᵥ b ∈ a +ᵥ s

theorem Set.smul_mem_smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} {b : β} : b ∈ s → a • b ∈ a • s

@[simp]

theorem Set.vadd_set_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} : a +ᵥ ∅ = ∅

@[simp]

theorem Set.smul_set_empty {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} : a • ∅ = ∅

@[simp]

theorem Set.vadd_set_eq_empty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} : a +ᵥ s = ∅ ↔ s = ∅

@[simp]

theorem Set.smul_set_eq_empty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : a • s = ∅ ↔ s = ∅

@[simp]

theorem Set.vadd_set_nonempty {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {a : α} : (a +ᵥ s).Nonempty ↔ s.Nonempty

@[simp]

theorem Set.smul_set_nonempty {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : (a • s).Nonempty ↔ s.Nonempty

@[simp]

theorem Set.vadd_set_singleton {α : Type u_2} {β : Type u_3} [VAdd α β] {a : α} {b : β} : a +ᵥ {b} = {a +ᵥ b}

@[simp]

theorem Set.smul_set_singleton {α : Type u_2} {β : Type u_3} [SMul α β] {a : α} {b : β} : a • {b} = {a • b}

theorem Set.vadd_set_mono {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {t : Set β} {a : α} : s ⊆ t → a +ᵥ s ⊆ a +ᵥ t

theorem Set.smul_set_mono {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {t : Set β} {a : α} : s ⊆ t → a • s ⊆ a • t

theorem Set.vadd_set_subset_iff {α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set β} {t : Set β} {a : α} : a +ᵥ s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a +ᵥ b ∈ t

theorem Set.smul_set_subset_iff {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {t : Set β} {a : α} : a • s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a • b ∈ t

theorem Set.vadd_set_union {α : Type u_2} {β : Type u_3} [VAdd α β] {t₁ : Set β} {t₂ : Set β} {a : α} : a +ᵥ (t₁ ∪ t₂) = a +ᵥ t₁ ∪ (a +ᵥ t₂)

theorem Set.smul_set_union {α : Type u_2} {β : Type u_3} [SMul α β] {t₁ : Set β} {t₂ : Set β} {a : α} : a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂

theorem Set.vadd_set_inter_subset {α : Type u_2} {β : Type u_3} [VAdd α β] {t₁ : Set β} {t₂ : Set β} {a : α} : a +ᵥ t₁ ∩ t₂ ⊆ (a +ᵥ t₁) ∩ (a +ᵥ t₂)

theorem Set.smul_set_inter_subset {α : Type u_2} {β : Type u_3} [SMul α β] {t₁ : Set β} {t₂ : Set β} {a : α} : a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂

theorem Set.vadd_set_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (a : α) (s : ι → Set β) : a +ᵥ ⋃ (i : ι), s i = ⋃ (i : ι), a +ᵥ s i

theorem Set.smul_set_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (a : α) (s : ι → Set β) : a • ⋃ (i : ι), s i = ⋃ (i : ι), a • s i

theorem Set.vadd_set_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (a : α) (s : (i : ι) → κ i → Set β) : a +ᵥ ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), a +ᵥ s i j

theorem Set.smul_set_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [SMul α β] (a : α) (s : (i : ι) → κ i → Set β) : a • ⋃ (i : ι), ⋃ (j : κ i), s i j = ⋃ (i : ι), ⋃ (j : κ i), a • s i j

theorem Set.vadd_set_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VAdd α β] (a : α) (t : ι → Set β) : a +ᵥ ⋂ (i : ι), t i ⊆ ⋂ (i : ι), a +ᵥ t i

theorem Set.smul_set_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [SMul α β] (a : α) (t : ι → Set β) : a • ⋂ (i : ι), t i ⊆ ⋂ (i : ι), a • t i

theorem Set.vadd_set_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VAdd α β] (a : α) (t : (i : ι) → κ i → Set β) : a +ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), a +ᵥ t i j

theorem Set.smul_set_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [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} [VAdd α β] {s : Set β} {a : α} : s.Nonempty → (a +ᵥ s).Nonempty

theorem Set.Nonempty.smul_set {α : Type u_2} {β : Type u_3} [SMul α β] {s : Set β} {a : α} : s.Nonempty → (a • s).Nonempty

theorem Set.range_vadd_range {α : Type u_2} {β : Type u_3} {ι : Type u_5} {κ : Type u_6} [VAdd α β] (b : ι → α) (c : κ → β) : Set.range b +ᵥ Set.range c = Set.range fun (p : ι × κ) => b p.1 +ᵥ c p.2

theorem Set.range_smul_range {α : Type u_2} {β : Type u_3} {ι : Type u_5} {κ : Type u_6} [SMul α β] (b : ι → α) (c : κ → β) : Set.range b • Set.range c = Set.range fun (p : ι × κ) => b p.1 • c p.2

theorem Set.vadd_set_range {α : Type u_2} {β : Type u_3} [VAdd α β] {ι : Sort u_5} (a : α) (f : ι → β) : a +ᵥ Set.range f = Set.range fun (i : ι) => a +ᵥ f i

theorem Set.smul_set_range {α : Type u_2} {β : Type u_3} [SMul α β] {ι : Sort u_5} (a : α) (f : ι → β) : a • Set.range f = Set.range fun (i : ι) => a • f i

theorem Set.range_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] {ι : Sort u_5} (a : α) (f : ι → β) : (Set.range fun (i : ι) => a +ᵥ f i) = a +ᵥ Set.range f

theorem Set.range_smul {α : Type u_2} {β : Type u_3} [SMul α β] {ι : Sort u_5} (a : α) (f : ι → β) : (Set.range fun (i : ι) => a • f i) = a • Set.range f

instance Set.vsub {α : Type u_2} {β : Type u_3} [VSub α β] : VSub (Set α) (Set β)

Equations

• Set.vsub = { vsub := Set.image2 fun (x1 x2 : β) => x1 -ᵥ x2 }

@[simp]

theorem Set.image2_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : Set.image2 VSub.vsub s t = s -ᵥ t

theorem Set.image_vsub_prod {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : (fun (x : β × β) => x.1 -ᵥ x.2) '' s ×ˢ t = s -ᵥ t

theorem Set.mem_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} {a : α} : a ∈ s -ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x -ᵥ y = a

theorem Set.vsub_mem_vsub {α : Type u_2} {β : Type u_3} [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_3} [VSub α β] (t : Set β) : ∅ -ᵥ t = ∅

@[simp]

theorem Set.vsub_empty {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) : s -ᵥ ∅ = ∅

@[simp]

theorem Set.vsub_eq_empty {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅

@[simp]

theorem Set.vsub_nonempty {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : (s -ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

theorem Set.Nonempty.vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty

theorem Set.Nonempty.of_vsub_left {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : (s -ᵥ t).Nonempty → s.Nonempty

theorem Set.Nonempty.of_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : (s -ᵥ t).Nonempty → t.Nonempty

@[simp]

theorem Set.vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] (s : Set β) (b : β) : s -ᵥ {b} = (fun (x : β) => x -ᵥ b) '' s

@[simp]

theorem Set.singleton_vsub {α : Type u_2} {β : Type u_3} [VSub α β] (t : Set β) (b : β) : {b} -ᵥ t = (fun (x : β) => b -ᵥ x) '' t

@[simp]

theorem Set.singleton_vsub_singleton {α : Type u_2} {β : Type u_3} [VSub α β] {b : β} {c : β} : {b} -ᵥ {c} = {b -ᵥ c}

theorem Set.vsub_subset_vsub {α : Type u_2} {β : Type u_3} [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_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} : t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂

theorem Set.vsub_subset_vsub_right {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} : s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t

theorem Set.vsub_subset_iff {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} {u : Set α} : s -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u

theorem Set.vsub_self_mono {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} (h : s ⊆ t) : s -ᵥ s ⊆ t -ᵥ t

theorem Set.union_vsub {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} : s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)

theorem Set.vsub_union {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} : s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)

theorem Set.inter_vsub_subset {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t : Set β} : s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)

theorem Set.vsub_inter_subset {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t₁ : Set β} {t₂ : Set β} : s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)

theorem Set.inter_vsub_union_subset_union {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} : s₁ ∩ s₂ -ᵥ (t₁ ∪ t₂) ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)

theorem Set.union_vsub_inter_subset_union {α : Type u_2} {β : Type u_3} [VSub α β] {s₁ : Set β} {s₂ : Set β} {t₁ : Set β} {t₂ : Set β} : s₁ ∪ s₂ -ᵥ t₁ ∩ t₂ ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)

theorem Set.iUnion_vsub_left_image {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : ⋃ a ∈ s, (fun (x : β) => a -ᵥ x) '' t = s -ᵥ t

theorem Set.iUnion_vsub_right_image {α : Type u_2} {β : Type u_3} [VSub α β] {s : Set β} {t : Set β} : ⋃ a ∈ t, (fun (x : β) => x -ᵥ a) '' s = s -ᵥ t

theorem Set.iUnion_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : ι → Set β) (t : Set β) : (⋃ (i : ι), s i) -ᵥ t = ⋃ (i : ι), s i -ᵥ t

theorem Set.vsub_iUnion {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : Set β) (t : ι → Set β) : s -ᵥ ⋃ (i : ι), t i = ⋃ (i : ι), s -ᵥ t i

theorem Set.iUnion₂_vsub {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VSub α β] (s : (i : ι) → κ i → Set β) (t : Set β) : (⋃ (i : ι), ⋃ (j : κ i), s i j) -ᵥ t = ⋃ (i : ι), ⋃ (j : κ i), s i j -ᵥ t

theorem Set.vsub_iUnion₂ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VSub α β] (s : Set β) (t : (i : ι) → κ i → Set β) : s -ᵥ ⋃ (i : ι), ⋃ (j : κ i), t i j = ⋃ (i : ι), ⋃ (j : κ i), s -ᵥ t i j

theorem Set.iInter_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : ι → Set β) (t : Set β) : (⋂ (i : ι), s i) -ᵥ t ⊆ ⋂ (i : ι), s i -ᵥ t

theorem Set.vsub_iInter_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [VSub α β] (s : Set β) (t : ι → Set β) : s -ᵥ ⋂ (i : ι), t i ⊆ ⋂ (i : ι), s -ᵥ t i

theorem Set.iInter₂_vsub_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VSub α β] (s : (i : ι) → κ i → Set β) (t : Set β) : (⋂ (i : ι), ⋂ (j : κ i), s i j) -ᵥ t ⊆ ⋂ (i : ι), ⋂ (j : κ i), s i j -ᵥ t

theorem Set.vsub_iInter₂_subset {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [VSub α β] (s : Set β) (t : (i : ι) → κ i → Set β) : s -ᵥ ⋂ (i : ι), ⋂ (j : κ i), t i j ⊆ ⋂ (i : ι), ⋂ (j : κ i), s -ᵥ t i j

theorem Set.image_vadd_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α β] [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_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] (f : β → γ) (a : α) (s : Set β) : (∀ (b : β), f (a • b) = a • f b) → f '' (a • s) = a • f '' s

def Set.NSMul {α : Type u_2} [Zero α] [Add α] : SMul ℕ (Set α)

Repeated pointwise addition (not the same as pointwise repeated addition!) of a Set. See note [pointwise nat action].

Equations

• Set.NSMul = { smul := nsmulRec }

def Set.NPow {α : Type u_2} [One α] [Mul α] : Pow (Set α) ℕ

Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a Set. See note [pointwise nat action].

Equations

• Set.NPow = { pow := fun (s : Set α) (n : ℕ) => npowRec n s }

def Set.ZSMul {α : Type u_2} [Zero α] [Add α] [Neg α] : SMul ℤ (Set α)

Repeated pointwise addition/subtraction (not the same as pointwise repeated addition/subtraction!) of a Set. See note [pointwise nat action].

Equations

• Set.ZSMul = { smul := zsmulRec }

def Set.ZPow {α : Type u_2} [One α] [Mul α] [Inv α] : Pow (Set α) ℤ

Repeated pointwise multiplication/division (not the same as pointwise repeated multiplication/division!) of a Set. See note [pointwise nat action].

Equations

• Set.ZPow = { pow := fun (s : Set α) (n : ℤ) => zpowRec npowRec n s }

noncomputable def Set.addSemigroup {α : Type u_2} [AddSemigroup α] : AddSemigroup (Set α)

Set α is an AddSemigroup under pointwise operations if α is.

Equations

• Set.addSemigroup = AddSemigroup.mk ⋯

theorem Set.addSemigroup.proof_1 {α : Type u_1} [AddSemigroup α] : ∀ (x x_1 x_2 : Set α), Set.image2 (fun (x1 x2 : α) => x1 + x2) (Set.image2 (fun (x1 x2 : α) => x1 + x2) x x_1) x_2 = Set.image2 (fun (x1 x2 : α) => x1 + x2) x (Set.image2 (fun (x1 x2 : α) => x1 + x2) x_1 x_2)

noncomputable def Set.semigroup {α : Type u_2} [Semigroup α] : Semigroup (Set α)

Set α is a Semigroup under pointwise operations if α is.

Equations

• Set.semigroup = Semigroup.mk ⋯

noncomputable def Set.addCommSemigroup {α : Type u_2} [AddCommSemigroup α] : AddCommSemigroup (Set α)

Set α is an AddCommSemigroup under pointwise operations if α is.

Equations

• Set.addCommSemigroup = AddCommSemigroup.mk ⋯

theorem Set.addCommSemigroup.proof_1 {α : Type u_1} [AddCommSemigroup α] : ∀ (x x_1 : Set α), Set.image2 (fun (x1 x2 : α) => x1 + x2) x x_1 = Set.image2 (fun (x1 x2 : α) => x1 + x2) x_1 x

noncomputable def Set.commSemigroup {α : Type u_2} [CommSemigroup α] : CommSemigroup (Set α)

Set α is a CommSemigroup under pointwise operations if α is.

Equations

• Set.commSemigroup = CommSemigroup.mk ⋯

theorem Set.inter_add_union_subset {α : Type u_2} [AddCommSemigroup α] {s : Set α} {t : Set α} : s ∩ t + (s ∪ t) ⊆ s + t

theorem Set.inter_mul_union_subset {α : Type u_2} [CommSemigroup α] {s : Set α} {t : Set α} : s ∩ t * (s ∪ t) ⊆ s * t

theorem Set.union_add_inter_subset {α : Type u_2} [AddCommSemigroup α] {s : Set α} {t : Set α} : s ∪ t + s ∩ t ⊆ s + t

theorem Set.union_mul_inter_subset {α : Type u_2} [CommSemigroup α] {s : Set α} {t : Set α} : (s ∪ t) * (s ∩ t) ⊆ s * t

theorem Set.addZeroClass.proof_2 {α : Type u_1} [AddZeroClass α] (s : Set α) : Set.image2 (fun (x1 x2 : α) => x1 + x2) s {0} = s

theorem Set.addZeroClass.proof_1 {α : Type u_1} [AddZeroClass α] (t : Set α) : Set.image2 (fun (x1 x2 : α) => x1 + x2) {0} t = t

noncomputable def Set.addZeroClass {α : Type u_2} [AddZeroClass α] : AddZeroClass (Set α)

Set α is an AddZeroClass under pointwise operations if α is.

Equations

• Set.addZeroClass = AddZeroClass.mk ⋯ ⋯

noncomputable def Set.mulOneClass {α : Type u_2} [MulOneClass α] : MulOneClass (Set α)

Set α is a MulOneClass under pointwise operations if α is.

Equations

• Set.mulOneClass = MulOneClass.mk ⋯ ⋯

theorem Set.subset_add_left {α : Type u_2} [AddZeroClass α] (s : Set α) {t : Set α} (ht : 0 ∈ t) : s ⊆ s + t

theorem Set.subset_mul_left {α : Type u_2} [MulOneClass α] (s : Set α) {t : Set α} (ht : 1 ∈ t) : s ⊆ s * t

theorem Set.subset_add_right {α : Type u_2} [AddZeroClass α] {s : Set α} (t : Set α) (hs : 0 ∈ s) : t ⊆ s + t

theorem Set.subset_mul_right {α : Type u_2} [MulOneClass α] {s : Set α} (t : Set α) (hs : 1 ∈ s) : t ⊆ s * t

theorem Set.singletonAddMonoidHom.proof_1 {α : Type u_1} [AddZeroClass α] : Set.singletonZeroHom.toFun 0 = 0

theorem Set.singletonAddMonoidHom.proof_2 {α : Type u_1} [AddZeroClass α] (x : α) (y : α) : Set.singletonAddHom.toFun (x + y) = Set.singletonAddHom.toFun x + Set.singletonAddHom.toFun y

noncomputable def Set.singletonAddMonoidHom {α : Type u_2} [AddZeroClass α] : α →+ Set α

The singleton operation as an AddMonoidHom.

Equations

• Set.singletonAddMonoidHom = { toFun := Set.singletonAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def Set.singletonMonoidHom {α : Type u_2} [MulOneClass α] : α →* Set α

The singleton operation as a MonoidHom.

Equations

• Set.singletonMonoidHom = { toFun := Set.singletonMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Set.coe_singletonAddMonoidHom {α : Type u_2} [AddZeroClass α] : ⇑Set.singletonAddMonoidHom = singleton

@[simp]

theorem Set.coe_singletonMonoidHom {α : Type u_2} [MulOneClass α] : ⇑Set.singletonMonoidHom = singleton

@[simp]

theorem Set.singletonAddMonoidHom_apply {α : Type u_2} [AddZeroClass α] (a : α) : Set.singletonAddMonoidHom a = {a}

@[simp]

theorem Set.singletonMonoidHom_apply {α : Type u_2} [MulOneClass α] (a : α) : Set.singletonMonoidHom a = {a}

theorem Set.addMonoid.proof_2 {α : Type u_1} [AddMonoid α] (a : Set α) : a + 0 = a

noncomputable def Set.addMonoid {α : Type u_2} [AddMonoid α] : AddMonoid (Set α)

Set α is an AddMonoid under pointwise operations if α is.

Equations

• Set.addMonoid = AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

theorem Set.addMonoid.proof_4 {α : Type u_1} [AddMonoid α] : ∀ (n : ℕ) (x : Set α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem Set.addMonoid.proof_3 {α : Type u_1} [AddMonoid α] : ∀ (x : Set α), nsmulRec 0 x = nsmulRec 0 x

theorem Set.addMonoid.proof_1 {α : Type u_1} [AddMonoid α] (a : Set α) : 0 + a = a

noncomputable def Set.monoid {α : Type u_2} [Monoid α] : Monoid (Set α)

Set α is a Monoid under pointwise operations if α is.

Equations

• Set.monoid = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

theorem Set.nsmul_mem_nsmul {α : Type u_2} [AddMonoid α] {s : Set α} {a : α} (ha : a ∈ s) (n : ℕ) : n • a ∈ n • s

theorem Set.pow_mem_pow {α : Type u_2} [Monoid α] {s : Set α} {a : α} (ha : a ∈ s) (n : ℕ) : a ^ n ∈ s ^ n

theorem Set.nsmul_subset_nsmul {α : Type u_2} [AddMonoid α] {s : Set α} {t : Set α} (hst : s ⊆ t) (n : ℕ) : n • s ⊆ n • t

theorem Set.pow_subset_pow {α : Type u_2} [Monoid α] {s : Set α} {t : Set α} (hst : s ⊆ t) (n : ℕ) : s ^ n ⊆ t ^ n

theorem Set.nsmul_subset_nsmul_of_zero_mem {α : Type u_2} [AddMonoid α] {s : Set α} {m : ℕ} {n : ℕ} (hs : 0 ∈ s) (hn : m ≤ n) : m • s ⊆ n • s

theorem Set.pow_subset_pow_of_one_mem {α : Type u_2} [Monoid α] {s : Set α} {m : ℕ} {n : ℕ} (hs : 1 ∈ s) (hn : m ≤ n) : s ^ m ⊆ s ^ n

@[simp]

theorem Set.empty_nsmul {α : Type u_2} [AddMonoid α] {n : ℕ} (hn : n ≠ 0) : n • ∅ = ∅

@[simp]

theorem Set.empty_pow {α : Type u_2} [Monoid α] {n : ℕ} (hn : n ≠ 0) : ∅ ^ n = ∅

theorem Set.add_univ_of_zero_mem {α : Type u_2} [AddMonoid α] {s : Set α} (hs : 0 ∈ s) : s + Set.univ = Set.univ

theorem Set.mul_univ_of_one_mem {α : Type u_2} [Monoid α] {s : Set α} (hs : 1 ∈ s) : s * Set.univ = Set.univ

theorem Set.univ_add_of_zero_mem {α : Type u_2} [AddMonoid α] {t : Set α} (ht : 0 ∈ t) : Set.univ + t = Set.univ

theorem Set.univ_mul_of_one_mem {α : Type u_2} [Monoid α] {t : Set α} (ht : 1 ∈ t) : Set.univ * t = Set.univ

@[simp]

theorem Set.univ_add_univ {α : Type u_2} [AddMonoid α] : Set.univ + Set.univ = Set.univ

@[simp]

theorem Set.univ_mul_univ {α : Type u_2} [Monoid α] : Set.univ * Set.univ = Set.univ

@[simp]

theorem Set.nsmul_univ {α : Type u_2} [AddMonoid α] {n : ℕ} : n ≠ 0 → n • Set.univ = Set.univ

@[simp]

theorem Set.univ_pow {α : Type u_2} [Monoid α] {n : ℕ} : n ≠ 0 → Set.univ ^ n = Set.univ

theorem IsAddUnit.set {α : Type u_2} [AddMonoid α] {a : α} : IsAddUnit a → IsAddUnit {a}

theorem IsUnit.set {α : Type u_2} [Monoid α] {a : α} : IsUnit a → IsUnit {a}

noncomputable def Set.addCommMonoid {α : Type u_2} [AddCommMonoid α] : AddCommMonoid (Set α)

Set α is an AddCommMonoid under pointwise operations if α is.

Equations

• Set.addCommMonoid = AddCommMonoid.mk ⋯

theorem Set.addCommMonoid.proof_1 {α : Type u_1} [AddCommMonoid α] (a : Set α) (b : Set α) : a + b = b + a

noncomputable def Set.commMonoid {α : Type u_2} [CommMonoid α] : CommMonoid (Set α)

Set α is a CommMonoid under pointwise operations if α is.

Equations

• Set.commMonoid = CommMonoid.mk ⋯

theorem Set.add_eq_zero_iff {α : Type u_2} [SubtractionMonoid α] {s : Set α} {t : Set α} : s + t = 0 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a + b = 0

theorem Set.mul_eq_one_iff {α : Type u_2} [DivisionMonoid α] {s : Set α} {t : Set α} : s * t = 1 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a * b = 1

theorem Set.subtractionMonoid.proof_3 {α : Type u_1} [SubtractionMonoid α] : ∀ (n : ℕ) (a : Set α), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a

theorem Set.subtractionMonoid.proof_6 {α : Type u_1} [SubtractionMonoid α] (s : Set α) (t : Set α) : -(s + t) = -t + -s

theorem Set.subtractionMonoid.proof_7 {α : Type u_1} [SubtractionMonoid α] (s : Set α) (t : Set α) (h : s + t = 0) : -s = t

theorem Set.subtractionMonoid.proof_2 {α : Type u_1} [SubtractionMonoid α] : ∀ (a : Set α), zsmulRec 0 a = zsmulRec 0 a

theorem Set.subtractionMonoid.proof_1 {α : Type u_1} [SubtractionMonoid α] (s : Set α) (t : Set α) : s - t = s + -t

theorem Set.subtractionMonoid.proof_4 {α : Type u_1} [SubtractionMonoid α] : ∀ (n : ℕ) (a : Set α), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

noncomputable def Set.subtractionMonoid {α : Type u_2} [SubtractionMonoid α] : SubtractionMonoid (Set α)

Set α is a subtraction monoid under pointwise operations if α is.

Equations

• Set.subtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯

theorem Set.subtractionMonoid.proof_5 {α : Type u_1} [SubtractionMonoid α] (x : Set α) : - -x = x

noncomputable def Set.divisionMonoid {α : Type u_2} [DivisionMonoid α] : DivisionMonoid (Set α)

Set α is a division monoid under pointwise operations if α is.

Equations

• Set.divisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯

@[simp]

theorem Set.isAddUnit_iff {α : Type u_2} [SubtractionMonoid α] {s : Set α} : IsAddUnit s ↔ ∃ (a : α), s = {a} ∧ IsAddUnit a

@[simp]

theorem Set.isUnit_iff {α : Type u_2} [DivisionMonoid α] {s : Set α} : IsUnit s ↔ ∃ (a : α), s = {a} ∧ IsUnit a

@[simp]

theorem Set.univ_sub_univ {α : Type u_2} [SubtractionMonoid α] : Set.univ - Set.univ = Set.univ

@[simp]

theorem Set.univ_div_univ {α : Type u_2} [DivisionMonoid α] : Set.univ / Set.univ = Set.univ

theorem Set.subtractionCommMonoid.proof_1 {α : Type u_1} [SubtractionCommMonoid α] (a : Set α) (b : Set α) : a + b = b + a

noncomputable def Set.subtractionCommMonoid {α : Type u_2} [SubtractionCommMonoid α] : SubtractionCommMonoid (Set α)

Set α is a commutative subtraction monoid under pointwise operations if α is.

Equations

• Set.subtractionCommMonoid = SubtractionCommMonoid.mk ⋯

noncomputable def Set.divisionCommMonoid {α : Type u_2} [DivisionCommMonoid α] : DivisionCommMonoid (Set α)

Set α is a commutative division monoid under pointwise operations if α is.

Equations

• Set.divisionCommMonoid = DivisionCommMonoid.mk ⋯

Note that Set is not a Group because s / s ≠ 1 in general.

@[simp]

theorem Set.zero_mem_sub_iff {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} : 0 ∈ s - t ↔ ¬Disjoint s t

@[simp]

theorem Set.one_mem_div_iff {α : Type u_2} [Group α] {s : Set α} {t : Set α} : 1 ∈ s / t ↔ ¬Disjoint s t

theorem Set.not_zero_mem_sub_iff {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} : 0 ∉ s - t ↔ Disjoint s t

theorem Set.not_one_mem_div_iff {α : Type u_2} [Group α] {s : Set α} {t : Set α} : 1 ∉ s / t ↔ Disjoint s t

theorem Disjoint.one_not_mem_div_set {α : Type u_2} [Group α] {s : Set α} {t : Set α} : Disjoint s t → 1 ∉ s / t

Alias of the reverse direction of Set.not_one_mem_div_iff.

theorem Disjoint.zero_not_mem_sub_set {α : Type u_2} [AddGroup α] {s : Set α} {t : Set α} : Disjoint s t → 0 ∉ s - t

theorem Set.Nonempty.zero_mem_sub {α : Type u_2} [AddGroup α] {s : Set α} (h : s.Nonempty) : 0 ∈ s - s

theorem Set.Nonempty.one_mem_div {α : Type u_2} [Group α] {s : Set α} (h : s.Nonempty) : 1 ∈ s / s

theorem Set.isAddUnit_singleton {α : Type u_2} [AddGroup α] (a : α) : IsAddUnit {a}

theorem Set.isUnit_singleton {α : Type u_2} [Group α] (a : α) : IsUnit {a}

@[simp]

theorem Set.isAddUnit_iff_singleton {α : Type u_2} [AddGroup α] {s : Set α} : IsAddUnit s ↔ ∃ (a : α), s = {a}

@[simp]

theorem Set.isUnit_iff_singleton {α : Type u_2} [Group α] {s : Set α} : IsUnit s ↔ ∃ (a : α), s = {a}

@[simp]

theorem Set.image_add_left {α : Type u_2} [AddGroup α] {t : Set α} {a : α} : (fun (x : α) => a + x) '' t = (fun (x : α) => -a + x) ⁻¹' t

@[simp]

theorem Set.image_mul_left {α : Type u_2} [Group α] {t : Set α} {a : α} : (fun (x : α) => a * x) '' t = (fun (x : α) => a⁻¹ * x) ⁻¹' t

@[simp]

theorem Set.image_add_right {α : Type u_2} [AddGroup α] {t : Set α} {b : α} : (fun (x : α) => x + b) '' t = (fun (x : α) => x + -b) ⁻¹' t

@[simp]

theorem Set.image_mul_right {α : Type u_2} [Group α] {t : Set α} {b : α} : (fun (x : α) => x * b) '' t = (fun (x : α) => x * b⁻¹) ⁻¹' t

theorem Set.image_add_left' {α : Type u_2} [AddGroup α] {t : Set α} {a : α} : (fun (x : α) => -a + x) '' t = (fun (x : α) => a + x) ⁻¹' t

theorem Set.image_mul_left' {α : Type u_2} [Group α] {t : Set α} {a : α} : (fun (x : α) => a⁻¹ * x) '' t = (fun (x : α) => a * x) ⁻¹' t

theorem Set.image_add_right' {α : Type u_2} [AddGroup α] {t : Set α} {b : α} : (fun (x : α) => x + -b) '' t = (fun (x : α) => x + b) ⁻¹' t

theorem Set.image_mul_right' {α : Type u_2} [Group α] {t : Set α} {b : α} : (fun (x : α) => x * b⁻¹) '' t = (fun (x : α) => x * b) ⁻¹' t

@[simp]

theorem Set.preimage_add_left_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} : (fun (x : α) => a + x) ⁻¹' {b} = {-a + b}

@[simp]

theorem Set.preimage_mul_left_singleton {α : Type u_2} [Group α] {a : α} {b : α} : (fun (x : α) => a * x) ⁻¹' {b} = {a⁻¹ * b}

@[simp]

theorem Set.preimage_add_right_singleton {α : Type u_2} [AddGroup α] {a : α} {b : α} : (fun (x : α) => x + a) ⁻¹' {b} = {b + -a}

@[simp]

theorem Set.preimage_mul_right_singleton {α : Type u_2} [Group α] {a : α} {b : α} : (fun (x : α) => x * a) ⁻¹' {b} = {b * a⁻¹}

@[simp]

theorem Set.preimage_add_left_zero {α : Type u_2} [AddGroup α] {a : α} : (fun (x : α) => a + x) ⁻¹' 0 = {-a}

@[simp]

theorem Set.preimage_mul_left_one {α : Type u_2} [Group α] {a : α} : (fun (x : α) => a * x) ⁻¹' 1 = {a⁻¹}

@[simp]

theorem Set.preimage_add_right_zero {α : Type u_2} [AddGroup α] {b : α} : (fun (x : α) => x + b) ⁻¹' 0 = {-b}

@[simp]

theorem Set.preimage_mul_right_one {α : Type u_2} [Group α] {b : α} : (fun (x : α) => x * b) ⁻¹' 1 = {b⁻¹}

theorem Set.preimage_add_left_zero' {α : Type u_2} [AddGroup α] {a : α} : (fun (x : α) => -a + x) ⁻¹' 0 = {a}

theorem Set.preimage_mul_left_one' {α : Type u_2} [Group α] {a : α} : (fun (x : α) => a⁻¹ * x) ⁻¹' 1 = {a}

theorem Set.preimage_add_right_zero' {α : Type u_2} [AddGroup α] {b : α} : (fun (x : α) => x + -b) ⁻¹' 0 = {b}

theorem Set.preimage_mul_right_one' {α : Type u_2} [Group α] {b : α} : (fun (x : α) => x * b⁻¹) ⁻¹' 1 = {b}

@[simp]

theorem Set.add_univ {α : Type u_2} [AddGroup α] {s : Set α} (hs : s.Nonempty) : s + Set.univ = Set.univ

@[simp]

theorem Set.mul_univ {α : Type u_2} [Group α] {s : Set α} (hs : s.Nonempty) : s * Set.univ = Set.univ

@[simp]

theorem Set.univ_add {α : Type u_2} [AddGroup α] {t : Set α} (ht : t.Nonempty) : Set.univ + t = Set.univ

@[simp]

theorem Set.univ_mul {α : Type u_2} [Group α] {t : Set α} (ht : t.Nonempty) : Set.univ * t = Set.univ

theorem Set.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) {s : Set α} {t : Set α} : ⇑m '' (s + t) = ⇑m '' s + ⇑m '' t

theorem Set.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) {s : Set α} {t : Set α} : ⇑m '' (s * t) = ⇑m '' s * ⇑m '' t

theorem Set.add_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) {s : Set β} {t : Set β} (hs : s ⊆ Set.range ⇑m) (ht : t ⊆ Set.range ⇑m) : s + t ⊆ Set.range ⇑m

theorem Set.mul_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) {s : Set β} {t : Set β} (hs : s ⊆ Set.range ⇑m) (ht : t ⊆ Set.range ⇑m) : s * t ⊆ Set.range ⇑m

theorem Set.preimage_add_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) {s : Set β} {t : Set β} : ⇑m ⁻¹' s + ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s + t)

theorem Set.preimage_mul_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) {s : Set β} {t : Set β} : ⇑m ⁻¹' s * ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s * t)

theorem Set.preimage_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) (hm : Function.Injective ⇑m) {s : Set β} {t : Set β} (hs : s ⊆ Set.range ⇑m) (ht : t ⊆ Set.range ⇑m) : ⇑m ⁻¹' (s + t) = ⇑m ⁻¹' s + ⇑m ⁻¹' t

theorem Set.preimage_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) (hm : Function.Injective ⇑m) {s : Set β} {t : Set β} (hs : s ⊆ Set.range ⇑m) (ht : t ⊆ Set.range ⇑m) : ⇑m ⁻¹' (s * t) = ⇑m ⁻¹' s * ⇑m ⁻¹' t

theorem Set.image_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s : Set α} {t : Set α} : ⇑m '' (s - t) = ⇑m '' s - ⇑m '' t

theorem Set.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {s : Set α} {t : Set α} : ⇑m '' (s / t) = ⇑m '' s / ⇑m '' t

theorem Set.sub_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s : Set β} {t : Set β} (hs : s ⊆ Set.range ⇑m) (ht : t ⊆ Set.range ⇑m) : s - t ⊆ Set.range ⇑m

theorem Set.div_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {s : Set β} {t : Set β} (hs : s ⊆ Set.range ⇑m) (ht : t ⊆ Set.range ⇑m) : s / t ⊆ Set.range ⇑m

theorem Set.preimage_sub_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s : Set β} {t : Set β} : ⇑m ⁻¹' s - ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s - t)

theorem Set.preimage_div_preimage_subset {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {s : Set β} {t : Set β} : ⇑m ⁻¹' s / ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s / t)

theorem Set.preimage_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) (hm : Function.Injective ⇑m) {s : Set β} {t : Set β} (hs : s ⊆ Set.range ⇑m) (ht : t ⊆ Set.range ⇑m) : ⇑m ⁻¹' (s - t) = ⇑m ⁻¹' s - ⇑m ⁻¹' t

theorem Set.preimage_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) (hm : Function.Injective ⇑m) {s : Set β} {t : Set β} (hs : s ⊆ Set.range ⇑m) (ht : t ⊆ Set.range ⇑m) : ⇑m ⁻¹' (s / t) = ⇑m ⁻¹' s / ⇑m ⁻¹' t

Miscellaneous

theorem AddGroup.card_nsmul_eq_card_nsmul_card_univ_aux {f : ℕ → ℕ} (h1 : Monotone f) {B : ℕ} (h2 : ∀ (n : ℕ), f n ≤ B) (h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)) (k : ℕ) : B ≤ k → f k = f B

theorem Group.card_pow_eq_card_pow_card_univ_aux {f : ℕ → ℕ} (h1 : Monotone f) {B : ℕ} (h2 : ∀ (n : ℕ), f n ≤ B) (h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)) (k : ℕ) : B ≤ k → f k = f B