Documentation

Mathlib.Data.Set.Pointwise.Basic

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∈ s and y ∈ t∈ t.
• s + t: Addition, set of all x + y where x ∈ s∈ s and y ∈ t∈ t.
• s⁻¹⁻¹: Inversion, set of all x⁻¹⁻¹ where x ∈ s∈ s.
• -s: Negation, set of all -x where x ∈ s∈ s.
• s / t: Division, set of all x / y where x ∈ s∈ s and y ∈ t∈ t.
• s - t: Subtraction, set of all x - y where x ∈ s∈ s and y ∈ t∈ t.

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: (λ h, h * g) ⁻¹' s⁻¹' s, (λ h, g * h) ⁻¹' s⁻¹' s, (λ h, h * g⁻¹) ⁻¹' s⁻¹) ⁻¹' s⁻¹' s, (λ h, g⁻¹ * h) ⁻¹' s⁻¹ * h) ⁻¹' s⁻¹' 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 #

0/1 as sets #

noncomputable def Set.zero {α : Type u_1} [inst : 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_1} [inst : 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_1} [inst : Zero α] :
{0} = 0
theorem Set.singleton_one {α : Type u_1} [inst : One α] :
{1} = 1
@[simp]
theorem Set.mem_zero {α : Type u_1} [inst : Zero α] {a : α} :
a 0 a = 0
@[simp]
theorem Set.mem_one {α : Type u_1} [inst : One α] {a : α} :
a 1 a = 1
theorem Set.zero_mem_zero {α : Type u_1} [inst : Zero α] :
0 0
theorem Set.one_mem_one {α : Type u_1} [inst : One α] :
1 1
@[simp]
theorem Set.zero_subset {α : Type u_1} [inst : Zero α] {s : Set α} :
0 s 0 s
@[simp]
theorem Set.one_subset {α : Type u_1} [inst : One α] {s : Set α} :
1 s 1 s
theorem Set.zero_nonempty {α : Type u_1} [inst : Zero α] :
theorem Set.one_nonempty {α : Type u_1} [inst : One α] :
@[simp]
theorem Set.image_zero {α : Type u_2} {β : Type u_1} [inst : Zero α] {f : αβ} :
f '' 0 = {f 0}
@[simp]
theorem Set.image_one {α : Type u_2} {β : Type u_1} [inst : One α] {f : αβ} :
f '' 1 = {f 1}
theorem Set.subset_zero_iff_eq {α : Type u_1} [inst : Zero α] {s : Set α} :
s 0 s = s = 0
theorem Set.subset_one_iff_eq {α : Type u_1} [inst : One α] {s : Set α} :
s 1 s = s = 1
theorem Set.Nonempty.subset_zero_iff {α : Type u_1} [inst : Zero α] {s : Set α} (h : ) :
s 0 s = 0
theorem Set.Nonempty.subset_one_iff {α : Type u_1} [inst : One α] {s : Set α} (h : ) :
s 1 s = 1
noncomputable def Set.singletonZeroHom {α : Type u_1} [inst : Zero α] :
ZeroHom α (Set α)

The singleton operation as a ZeroHom.

Equations
• Set.singletonZeroHom = { toFun := singleton, map_zero' := (_ : {0} = 0) }
noncomputable def Set.singletonOneHom {α : Type u_1} [inst : One α] :
OneHom α (Set α)

The singleton operation as a OneHom.

Equations
• Set.singletonOneHom = { toFun := singleton, map_one' := (_ : {1} = 1) }
@[simp]
theorem Set.coe_singletonZeroHom {α : Type u_1} [inst : Zero α] :
Set.singletonZeroHom = singleton
@[simp]
theorem Set.coe_singletonOneHom {α : Type u_1} [inst : One α] :
Set.singletonOneHom = singleton

Set negation/inversion #

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

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

Equations
def Set.inv {α : Type u_1} [inst : Inv α] :
Inv (Set α)

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

Equations
@[simp]
theorem Set.mem_neg {α : Type u_1} [inst : Neg α] {s : Set α} {a : α} :
a -s -a s
@[simp]
theorem Set.mem_inv {α : Type u_1} [inst : Inv α] {s : Set α} {a : α} :
@[simp]
theorem Set.neg_preimage {α : Type u_1} [inst : Neg α] {s : Set α} :
Neg.neg ⁻¹' s = -s
@[simp]
theorem Set.inv_preimage {α : Type u_1} [inst : Inv α] {s : Set α} :
Inv.inv ⁻¹' s = s⁻¹
@[simp]
theorem Set.neg_empty {α : Type u_1} [inst : Neg α] :
@[simp]
theorem Set.inv_empty {α : Type u_1} [inst : Inv α] :
@[simp]
theorem Set.neg_univ {α : Type u_1} [inst : Neg α] :
-Set.univ = Set.univ
@[simp]
theorem Set.inv_univ {α : Type u_1} [inst : Inv α] :
Set.univ⁻¹ = Set.univ
@[simp]
theorem Set.inter_neg {α : Type u_1} [inst : Neg α] {s : Set α} {t : Set α} :
-(s t) = -s -t
@[simp]
theorem Set.inter_inv {α : Type u_1} [inst : Inv α] {s : Set α} {t : Set α} :
@[simp]
theorem Set.union_neg {α : Type u_1} [inst : Neg α] {s : Set α} {t : Set α} :
-(s t) = -s -t
@[simp]
theorem Set.union_inv {α : Type u_1} [inst : Inv α] {s : Set α} {t : Set α} :
@[simp]
theorem Set.interᵢ_neg {α : Type u_1} {ι : Sort u_2} [inst : Neg α] (s : ιSet α) :
(-Set.interᵢ fun i => s i) = Set.interᵢ fun i => -s i
@[simp]
theorem Set.interᵢ_inv {α : Type u_1} {ι : Sort u_2} [inst : Inv α] (s : ιSet α) :
(Set.interᵢ fun i => s i)⁻¹ = Set.interᵢ fun i => (s i)⁻¹
@[simp]
theorem Set.unionᵢ_neg {α : Type u_1} {ι : Sort u_2} [inst : Neg α] (s : ιSet α) :
(-Set.unionᵢ fun i => s i) = Set.unionᵢ fun i => -s i
@[simp]
theorem Set.unionᵢ_inv {α : Type u_1} {ι : Sort u_2} [inst : Inv α] (s : ιSet α) :
(Set.unionᵢ fun i => s i)⁻¹ = Set.unionᵢ fun i => (s i)⁻¹
@[simp]
theorem Set.compl_neg {α : Type u_1} [inst : Neg α] {s : Set α} :
-s = (-s)
@[simp]
theorem Set.compl_inv {α : Type u_1} [inst : Inv α] {s : Set α} :
theorem Set.neg_mem_neg {α : Type u_1} [inst : ] {s : Set α} {a : α} :
-a -s a s
theorem Set.inv_mem_inv {α : Type u_1} [inst : ] {s : Set α} {a : α} :
@[simp]
theorem Set.nonempty_neg {α : Type u_1} [inst : ] {s : Set α} :
@[simp]
theorem Set.nonempty_inv {α : Type u_1} [inst : ] {s : Set α} :
theorem Set.Nonempty.neg {α : Type u_1} [inst : ] {s : Set α} (h : ) :
theorem Set.Nonempty.inv {α : Type u_1} [inst : ] {s : Set α} (h : ) :
@[simp]
theorem Set.image_neg {α : Type u_1} [inst : ] {s : Set α} :
Neg.neg '' s = -s
@[simp]
theorem Set.image_inv {α : Type u_1} [inst : ] {s : Set α} :
Inv.inv '' s = s⁻¹
def Set.involutiveNeg.proof_1 {α : Type u_1} [inst : ] (s : Set α) :
(fun x => - -x) ⁻¹' s = s
Equations
noncomputable instance Set.involutiveNeg {α : Type u_1} [inst : ] :
Equations
noncomputable instance Set.involutiveInv {α : Type u_1} [inst : ] :
Equations
@[simp]
theorem Set.neg_subset_neg {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
-s -t s t
@[simp]
theorem Set.inv_subset_inv {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
theorem Set.neg_subset {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
-s t s -t
theorem Set.inv_subset {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
@[simp]
theorem Set.neg_singleton {α : Type u_1} [inst : ] (a : α) :
-{a} = {-a}
@[simp]
theorem Set.inv_singleton {α : Type u_1} [inst : ] (a : α) :
{a}⁻¹ = {a⁻¹}
@[simp]
theorem Set.neg_insert {α : Type u_1} [inst : ] (a : α) (s : Set α) :
-insert a s = insert (-a) (-s)
@[simp]
theorem Set.inv_insert {α : Type u_1} [inst : ] (a : α) (s : Set α) :
(insert a s)⁻¹ =
theorem Set.neg_range {α : Type u_2} [inst : ] {ι : Sort u_1} {f : ια} :
= Set.range fun i => -f i
theorem Set.inv_range {α : Type u_2} [inst : ] {ι : Sort u_1} {f : ια} :
()⁻¹ = Set.range fun i => (f i)⁻¹
theorem Set.image_op_neg {α : Type u_1} [inst : ] {s : Set α} :
theorem Set.image_op_inv {α : Type u_1} [inst : ] {s : Set α} :
MulOpposite.op '' s⁻¹ = (MulOpposite.op '' s)⁻¹

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

Equations
def Set.mul {α : Type u_1} [inst : Mul α] :
Mul (Set α)

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

Equations
@[simp]
theorem Set.image2_add {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
Set.image2 (fun x x_1 => x + x_1) s t = s + t
@[simp]
theorem Set.image2_mul {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
Set.image2 (fun x x_1 => x * x_1) s t = s * t
theorem Set.mem_add {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} {a : α} :
a s + t x y, x s y t x + y = a
theorem Set.mem_mul {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} {a : α} :
a s * t x y, x s y t x * y = a
theorem Set.add_mem_add {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} {a : α} {b : α} :
a sb ta + b s + t
theorem Set.mul_mem_mul {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} {a : α} {b : α} :
a sb ta * b s * t
theorem Set.add_image_prod {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
(fun x => x.fst + x.snd) '' s ×ˢ t = s + t
theorem Set.image_mul_prod {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
(fun x => x.fst * x.snd) '' s ×ˢ t = s * t
@[simp]
theorem Set.empty_add {α : Type u_1} [inst : Add α] {s : Set α} :
@[simp]
theorem Set.empty_mul {α : Type u_1} [inst : Mul α] {s : Set α} :
@[simp]
theorem Set.add_empty {α : Type u_1} [inst : Add α] {s : Set α} :
@[simp]
theorem Set.mul_empty {α : Type u_1} [inst : Mul α] {s : Set α} :
@[simp]
theorem Set.add_eq_empty {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
s + t = s = t =
@[simp]
theorem Set.mul_eq_empty {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
s * t = s = t =
@[simp]
theorem Set.add_nonempty {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
@[simp]
theorem Set.mul_nonempty {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
theorem Set.Nonempty.add {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
Set.Nonempty (s + t)
theorem Set.Nonempty.mul {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
Set.Nonempty (s * t)
theorem Set.Nonempty.of_add_left {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
Set.Nonempty (s + t)
theorem Set.Nonempty.of_mul_left {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
Set.Nonempty (s * t)
theorem Set.Nonempty.of_add_right {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
Set.Nonempty (s + t)
theorem Set.Nonempty.of_mul_right {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
Set.Nonempty (s * t)
@[simp]
theorem Set.add_singleton {α : Type u_1} [inst : Add α] {s : Set α} {b : α} :
s + {b} = (fun x => x + b) '' s
@[simp]
theorem Set.mul_singleton {α : Type u_1} [inst : Mul α] {s : Set α} {b : α} :
s * {b} = (fun x => x * b) '' s
@[simp]
theorem Set.singleton_add {α : Type u_1} [inst : Add α] {t : Set α} {a : α} :
{a} + t = (fun x x_1 => x + x_1) a '' t
@[simp]
theorem Set.singleton_mul {α : Type u_1} [inst : Mul α] {t : Set α} {a : α} :
{a} * t = (fun x x_1 => x * x_1) a '' t
theorem Set.singleton_add_singleton {α : Type u_1} [inst : Add α] {a : α} {b : α} :
{a} + {b} = {a + b}
theorem Set.singleton_mul_singleton {α : Type u_1} [inst : Mul α] {a : α} {b : α} :
{a} * {b} = {a * b}
theorem Set.add_subset_add {α : Type u_1} [inst : Add α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
s₁ t₁s₂ t₂s₁ + s₂ t₁ + t₂
theorem Set.mul_subset_mul {α : Type u_1} [inst : 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_1} [inst : Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
t₁ t₂s + t₁ s + t₂
theorem Set.mul_subset_mul_left {α : Type u_1} [inst : Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
t₁ t₂s * t₁ s * t₂
theorem Set.add_subset_add_right {α : Type u_1} [inst : Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂s₁ + t s₂ + t
theorem Set.mul_subset_mul_right {α : Type u_1} [inst : Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂s₁ * t s₂ * t
theorem Set.add_subset_iff {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} {u : Set α} :
s + t u ∀ (x : α), x s∀ (y : α), y tx + y u
theorem Set.mul_subset_iff {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} {u : Set α} :
s * t u ∀ (x : α), x s∀ (y : α), y tx * y u
theorem Set.union_add {α : Type u_1} [inst : Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂ + t = s₁ + t (s₂ + t)
theorem Set.union_mul {α : Type u_1} [inst : Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
(s₁ s₂) * t = s₁ * t s₂ * t
theorem Set.add_union {α : Type u_1} [inst : Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s + (t₁ t₂) = s + t₁ (s + t₂)
theorem Set.mul_union {α : Type u_1} [inst : Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s * (t₁ t₂) = s * t₁ s * t₂
theorem Set.inter_add_subset {α : Type u_1} [inst : Add α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂ + t (s₁ + t) (s₂ + t)
theorem Set.inter_mul_subset {α : Type u_1} [inst : Mul α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂ * t s₁ * t (s₂ * t)
theorem Set.add_inter_subset {α : Type u_1} [inst : Add α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s + t₁ t₂ (s + t₁) (s + t₂)
theorem Set.mul_inter_subset {α : Type u_1} [inst : Mul α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s * (t₁ t₂) s * t₁ (s * t₂)
theorem Set.unionᵢ_add_left_image {α : Type u_1} [inst : Add α] {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ᵢ_mul_left_image {α : Type u_1} [inst : Mul α] {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ᵢ_add_right_image {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x + a) '' s) = s + t
theorem Set.unionᵢ_mul_right_image {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x * a) '' s) = s * t
theorem Set.unionᵢ_add {α : Type u_1} {ι : Sort u_2} [inst : Add α] (s : ιSet α) (t : Set α) :
(Set.unionᵢ fun i => s i) + t = Set.unionᵢ fun i => s i + t
theorem Set.unionᵢ_mul {α : Type u_1} {ι : Sort u_2} [inst : Mul α] (s : ιSet α) (t : Set α) :
(Set.unionᵢ fun i => s i) * t = Set.unionᵢ fun i => s i * t
theorem Set.add_unionᵢ {α : Type u_1} {ι : Sort u_2} [inst : Add α] (s : Set α) (t : ιSet α) :
(s + Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s + t i
theorem Set.mul_unionᵢ {α : Type u_1} {ι : Sort u_2} [inst : Mul α] (s : Set α) (t : ιSet α) :
(s * Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s * t i
theorem Set.unionᵢ₂_add {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Add α] (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ᵢ₂_mul {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Mul α] (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.add_unionᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Add α] (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.mul_unionᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Mul α] (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ᵢ_add_subset {α : Type u_1} {ι : Sort u_2} [inst : Add α] (s : ιSet α) (t : Set α) :
(Set.interᵢ fun i => s i) + t Set.interᵢ fun i => s i + t
theorem Set.interᵢ_mul_subset {α : Type u_1} {ι : Sort u_2} [inst : Mul α] (s : ιSet α) (t : Set α) :
(Set.interᵢ fun i => s i) * t Set.interᵢ fun i => s i * t
theorem Set.add_interᵢ_subset {α : Type u_1} {ι : Sort u_2} [inst : Add α] (s : Set α) (t : ιSet α) :
(s + Set.interᵢ fun i => t i) Set.interᵢ fun i => s + t i
theorem Set.mul_interᵢ_subset {α : Type u_1} {ι : Sort u_2} [inst : Mul α] (s : Set α) (t : ιSet α) :
(s * Set.interᵢ fun i => t i) Set.interᵢ fun i => s * t i
theorem Set.interᵢ₂_add_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Add α] (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ᵢ₂_mul_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Mul α] (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.add_interᵢ₂_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Add α] (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.mul_interᵢ₂_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Mul α] (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
∀ (x x_1 : α), {x + x_1} = {x} + {x_1}
Equations
• (_ : {x + x} = {x} + {x}) = (_ : {x + x} = {x} + {x})
noncomputable def Set.singletonAddHom {α : Type u_1} [inst : Add α] :

The singleton operation as an AddHom.

Equations
• Set.singletonAddHom = { toFun := singleton, map_add' := (_ : ∀ (x x_1 : α), {x + x_1} = {x} + {x_1}) }
noncomputable def Set.singletonMulHom {α : Type u_1} [inst : Mul α] :
α →ₙ* Set α

The singleton operation as a MulHom.

Equations
• Set.singletonMulHom = { toFun := singleton, map_mul' := (_ : ∀ (x x_1 : α), {x * x_1} = {x} * {x_1}) }
@[simp]
@[simp]
theorem Set.coe_singletonMulHom {α : Type u_1} [inst : Mul α] :
Set.singletonMulHom = singleton
@[simp]
theorem Set.singletonAddHom_apply {α : Type u_1} [inst : Add α] (a : α) :
@[simp]
theorem Set.singletonMulHom_apply {α : Type u_1} [inst : Mul α] (a : α) :
Set.singletonMulHom a = {a}
@[simp]
theorem Set.image_op_add {α : Type u_1} [inst : Add α] {s : Set α} {t : Set α} :
@[simp]
theorem Set.image_op_mul {α : Type u_1} [inst : Mul α] {s : Set α} {t : Set α} :
MulOpposite.op '' (s * t) = MulOpposite.op '' t * MulOpposite.op '' s

Set subtraction/division #

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

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

Equations
def Set.div {α : Type u_1} [inst : Div α] :
Div (Set α)

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

Equations
@[simp]
theorem Set.image2_sub {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} :
Set.image2 Sub.sub s t = s - t
@[simp]
theorem Set.image2_div {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} :
Set.image2 Div.div s t = s / t
theorem Set.mem_sub {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} {a : α} :
a s - t x y, x s y t x - y = a
theorem Set.mem_div {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} {a : α} :
a s / t x y, x s y t x / y = a
theorem Set.sub_mem_sub {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} {a : α} {b : α} :
a sb ta - b s - t
theorem Set.div_mem_div {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} {a : α} {b : α} :
a sb ta / b s / t
theorem Set.sub_image_prod {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} :
(fun x => x.fst - x.snd) '' s ×ˢ t = s - t
theorem Set.image_div_prod {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} :
(fun x => x.fst / x.snd) '' s ×ˢ t = s / t
@[simp]
theorem Set.empty_sub {α : Type u_1} [inst : Sub α] {s : Set α} :
@[simp]
theorem Set.empty_div {α : Type u_1} [inst : Div α] {s : Set α} :
@[simp]
theorem Set.sub_empty {α : Type u_1} [inst : Sub α] {s : Set α} :
@[simp]
theorem Set.div_empty {α : Type u_1} [inst : Div α] {s : Set α} :
@[simp]
theorem Set.sub_eq_empty {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} :
s - t = s = t =
@[simp]
theorem Set.div_eq_empty {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} :
s / t = s = t =
@[simp]
theorem Set.sub_nonempty {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} :
@[simp]
theorem Set.div_nonempty {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} :
theorem Set.Nonempty.sub {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} :
Set.Nonempty (s - t)
theorem Set.Nonempty.div {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} :
Set.Nonempty (s / t)
theorem Set.Nonempty.of_sub_left {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} :
Set.Nonempty (s - t)
theorem Set.Nonempty.of_div_left {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} :
Set.Nonempty (s / t)
theorem Set.Nonempty.of_sub_right {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} :
Set.Nonempty (s - t)
theorem Set.Nonempty.of_div_right {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} :
Set.Nonempty (s / t)
@[simp]
theorem Set.sub_singleton {α : Type u_1} [inst : Sub α] {s : Set α} {b : α} :
s - {b} = (fun x => x - b) '' s
@[simp]
theorem Set.div_singleton {α : Type u_1} [inst : Div α] {s : Set α} {b : α} :
s / {b} = (fun x => x / b) '' s
@[simp]
theorem Set.singleton_sub {α : Type u_1} [inst : Sub α] {t : Set α} {a : α} :
{a} - t = (fun x x_1 => x - x_1) a '' t
@[simp]
theorem Set.singleton_div {α : Type u_1} [inst : Div α] {t : Set α} {a : α} :
{a} / t = (fun x x_1 => x / x_1) a '' t
theorem Set.singleton_sub_singleton {α : Type u_1} [inst : Sub α] {a : α} {b : α} :
{a} - {b} = {a - b}
theorem Set.singleton_div_singleton {α : Type u_1} [inst : Div α] {a : α} {b : α} :
{a} / {b} = {a / b}
theorem Set.sub_subset_sub {α : Type u_1} [inst : Sub α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
s₁ t₁s₂ t₂s₁ - s₂ t₁ - t₂
theorem Set.div_subset_div {α : Type u_1} [inst : 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_1} [inst : Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
t₁ t₂s - t₁ s - t₂
theorem Set.div_subset_div_left {α : Type u_1} [inst : Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
t₁ t₂s / t₁ s / t₂
theorem Set.sub_subset_sub_right {α : Type u_1} [inst : Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂s₁ - t s₂ - t
theorem Set.div_subset_div_right {α : Type u_1} [inst : Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂s₁ / t s₂ / t
theorem Set.sub_subset_iff {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} {u : Set α} :
s - t u ∀ (x : α), x s∀ (y : α), y tx - y u
theorem Set.div_subset_iff {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} {u : Set α} :
s / t u ∀ (x : α), x s∀ (y : α), y tx / y u
theorem Set.union_sub {α : Type u_1} [inst : Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂ - t = s₁ - t (s₂ - t)
theorem Set.union_div {α : Type u_1} [inst : Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
(s₁ s₂) / t = s₁ / t s₂ / t
theorem Set.sub_union {α : Type u_1} [inst : Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s - (t₁ t₂) = s - t₁ (s - t₂)
theorem Set.div_union {α : Type u_1} [inst : Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s / (t₁ t₂) = s / t₁ s / t₂
theorem Set.inter_sub_subset {α : Type u_1} [inst : Sub α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂ - t (s₁ - t) (s₂ - t)
theorem Set.inter_div_subset {α : Type u_1} [inst : Div α] {s₁ : Set α} {s₂ : Set α} {t : Set α} :
s₁ s₂ / t s₁ / t (s₂ / t)
theorem Set.sub_inter_subset {α : Type u_1} [inst : Sub α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s - t₁ t₂ (s - t₁) (s - t₂)
theorem Set.div_inter_subset {α : Type u_1} [inst : Div α] {s : Set α} {t₁ : Set α} {t₂ : Set α} :
s / (t₁ t₂) s / t₁ (s / t₂)
theorem Set.unionᵢ_sub_left_image {α : Type u_1} [inst : Sub α] {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ᵢ_div_left_image {α : Type u_1} [inst : Div α] {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ᵢ_sub_right_image {α : Type u_1} [inst : Sub α] {s : Set α} {t : Set α} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x - a) '' s) = s - t
theorem Set.unionᵢ_div_right_image {α : Type u_1} [inst : Div α] {s : Set α} {t : Set α} :
(Set.unionᵢ fun a => Set.unionᵢ fun h => (fun x => x / a) '' s) = s / t
theorem Set.unionᵢ_sub {α : Type u_1} {ι : Sort u_2} [inst : Sub α] (s : ιSet α) (t : Set α) :
(Set.unionᵢ fun i => s i) - t = Set.unionᵢ fun i => s i - t
theorem Set.unionᵢ_div {α : Type u_1} {ι : Sort u_2} [inst : Div α] (s : ιSet α) (t : Set α) :
(Set.unionᵢ fun i => s i) / t = Set.unionᵢ fun i => s i / t
theorem Set.sub_unionᵢ {α : Type u_1} {ι : Sort u_2} [inst : Sub α] (s : Set α) (t : ιSet α) :
(s - Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s - t i
theorem Set.div_unionᵢ {α : Type u_1} {ι : Sort u_2} [inst : Div α] (s : Set α) (t : ιSet α) :
(s / Set.unionᵢ fun i => t i) = Set.unionᵢ fun i => s / t i
theorem Set.unionᵢ₂_sub {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Sub α] (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ᵢ₂_div {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Div α] (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.sub_unionᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Sub α] (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.div_unionᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Div α] (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ᵢ_sub_subset {α : Type u_1} {ι : Sort u_2} [inst : Sub α] (s : ιSet α) (t : Set α) :
(Set.interᵢ fun i => s i) - t Set.interᵢ fun i => s i - t
theorem Set.interᵢ_div_subset {α : Type u_1} {ι : Sort u_2} [inst : Div α] (s : ιSet α) (t : Set α) :
(Set.interᵢ fun i => s i) / t Set.interᵢ fun i => s i / t
theorem Set.sub_interᵢ_subset {α : Type u_1} {ι : Sort u_2} [inst : Sub α] (s : Set α) (t : ιSet α) :
(s - Set.interᵢ fun i => t i) Set.interᵢ fun i => s - t i
theorem Set.div_interᵢ_subset {α : Type u_1} {ι : Sort u_2} [inst : Div α] (s : Set α) (t : ιSet α) :
(s / Set.interᵢ fun i => t i) Set.interᵢ fun i => s / t i
theorem Set.interᵢ₂_sub_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Sub α] (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ᵢ₂_div_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Div α] (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.sub_interᵢ₂_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Sub α] (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.div_interᵢ₂_subset {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : Div α] (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
def Set.NSMul {α : Type u_1} [inst : Zero α] [inst : 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_1} [inst : One α] [inst : 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 n => npowRec n s }
def Set.ZSMul {α : Type u_1} [inst : Zero α] [inst : Add α] [inst : 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_1} [inst : One α] [inst : Mul α] [inst : 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 n => zpowRec n s }
def Set.addSemigroup.proof_1 {α : Type u_1} [inst : ] :
∀ (x x_1 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.
noncomputable def Set.addSemigroup {α : Type u_1} [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.
noncomputable def Set.semigroup {α : Type u_1} [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.
def Set.addCommSemigroup.proof_2 {α : Type u_1} [inst : ] :
∀ (x x_1 : Set α), Set.image2 (fun x x_2 => x + x_2) x x_1 = Set.image2 (fun x x_2 => x + x_2) x_1 x
Equations
def Set.addCommSemigroup.proof_1 {α : Type u_1} [inst : ] (a : Set α) (b : Set α) (c : Set α) :
a + b + c = a + (b + c)
Equations
• (_ : ∀ (a b c : Set α), a + b + c = a + (b + c)) = (_ : ∀ (a b c : Set α), a + b + c = a + (b + c))
noncomputable def Set.addCommSemigroup {α : Type u_1} [inst : ] :

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

Equations
noncomputable def Set.commSemigroup {α : Type u_1} [inst : ] :

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

Equations
noncomputable def Set.addZeroClass {α : Type u_1} [inst : ] :

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

Equations
• Set.addZeroClass = let src := Set.zero; let src_1 := Set.add; AddZeroClass.mk (_ : ∀ (s : Set α), {0} + s = s) (_ : ∀ (s : Set α), s + {0} = s)
def Set.addZeroClass.proof_1 {α : Type u_1} [inst : ] (s : Set α) :
{0} + s = s
Equations
• (_ : {0} + s = s) = (_ : {0} + s = s)
def Set.addZeroClass.proof_2 {α : Type u_1} [inst : ] (s : Set α) :
s + {0} = s
Equations
• (_ : s + {0} = s) = (_ : s + {0} = s)
noncomputable def Set.mulOneClass {α : Type u_1} [inst : ] :

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

Equations
• Set.mulOneClass = let src := Set.one; let src_1 := Set.mul; MulOneClass.mk (_ : ∀ (s : Set α), {1} * s = s) (_ : ∀ (s : Set α), s * {1} = s)
theorem Set.subset_add_left {α : Type u_1} [inst : ] (s : Set α) {t : Set α} (ht : 0 t) :
s s + t
theorem Set.subset_mul_left {α : Type u_1} [inst : ] (s : Set α) {t : Set α} (ht : 1 t) :
s s * t
theorem Set.subset_add_right {α : Type u_1} [inst : ] {s : Set α} (t : Set α) (hs : 0 s) :
t s + t
theorem Set.subset_mul_right {α : Type u_1} [inst : ] {s : Set α} (t : Set α) (hs : 1 s) :
t s * t
noncomputable def Set.singletonAddMonoidHom {α : Type u_1} [inst : ] :
α →+ Set α

The singleton operation as an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
def Set.singletonAddMonoidHom.proof_2 {α : Type u_1} [inst : ] (x : α) (y : α) :
Equations
• One or more equations did not get rendered due to their size.
def Set.singletonAddMonoidHom.proof_1 {α : Type u_1} [inst : ] :
ZeroHom.toFun Set.singletonZeroHom 0 = 0
Equations
noncomputable def Set.singletonMonoidHom {α : Type u_1} [inst : ] :
α →* Set α

The singleton operation as a MonoidHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Set.coe_singletonAddMonoidHom {α : Type u_1} [inst : ] :
@[simp]
theorem Set.coe_singletonMonoidHom {α : Type u_1} [inst : ] :
Set.singletonMonoidHom = singleton
@[simp]
theorem Set.singletonAddMonoidHom_apply {α : Type u_1} [inst : ] (a : α) :
@[simp]
theorem Set.singletonMonoidHom_apply {α : Type u_1} [inst : ] (a : α) :
Set.singletonMonoidHom a = {a}
def Set.addMonoid.proof_3 {α : Type u_1} [inst : ] (a : Set α) :
a + 0 = a
Equations
• (_ : ∀ (a : Set α), a + 0 = a) = (_ : ∀ (a : Set α), a + 0 = a)
def Set.addMonoid.proof_5 {α : Type u_1} [inst : ] :
∀ (n : ) (x : Set α), nsmulRec (n + 1) x = nsmulRec (n + 1) x
Equations
• (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)
def Set.addMonoid.proof_2 {α : Type u_1} [inst : ] (a : Set α) :
0 + a = a
Equations
• (_ : ∀ (a : Set α), 0 + a = a) = (_ : ∀ (a : Set α), 0 + a = a)
noncomputable def Set.addMonoid {α : Type u_1} [inst : ] :

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

Equations
• Set.addMonoid = let src := Set.addSemigroup; let src_1 := Set.addZeroClass; let src_2 := Set.NSMul; AddMonoid.mk (_ : ∀ (a : Set α), 0 + a = a) (_ : ∀ (a : Set α), a + 0 = a) nsmulRec
def Set.addMonoid.proof_1 {α : Type u_1} [inst : ] (a : Set α) (b : Set α) (c : Set α) :
a + b + c = a + (b + c)
Equations
• (_ : ∀ (a b c : Set α), a + b + c = a + (b + c)) = (_ : ∀ (a b c : Set α), a + b + c = a + (b + c))
def Set.addMonoid.proof_4 {α : Type u_1} [inst : ] :
∀ (x : Set α), nsmulRec 0 x = nsmulRec 0 x
Equations
• (_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)
noncomputable def Set.monoid {α : Type u_1} [inst : ] :
Monoid (Set α)

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

Equations
• Set.monoid = let src := Set.semigroup; let src_1 := Set.mulOneClass; let src_2 := Set.NPow; Monoid.mk (_ : ∀ (a : Set α), 1 * a = a) (_ : ∀ (a : Set α), a * 1 = a) npowRec
theorem Set.nsmul_mem_nsmul {α : Type u_1} [inst : ] {s : Set α} {a : α} (ha : a s) (n : ) :
n a n s
abbrev Set.nsmul_mem_nsmul.match_1 (motive : ) :
(x : ) → (Unitmotive 0) → ((n : ) → motive ()) → motive x
Equations
theorem Set.pow_mem_pow {α : Type u_1} [inst : ] {s : Set α} {a : α} (ha : a s) (n : ) :
a ^ n s ^ n
theorem Set.nsmul_subset_nsmul {α : Type u_1} [inst : ] {s : Set α} {t : Set α} (hst : s t) (n : ) :
n s n t
theorem Set.pow_subset_pow {α : Type u_1} [inst : ] {s : Set α} {t : Set α} (hst : s t) (n : ) :
s ^ n t ^ n
theorem Set.nsmul_subset_nsmul_of_zero_mem {α : Type u_1} [inst : ] {s : Set α} {m : } {n : } (hs : 0 s) (hn : m n) :
m s n s
theorem Set.pow_subset_pow_of_one_mem {α : Type u_1} [inst : ] {s : Set α} {m : } {n : } (hs : 1 s) (hn : m n) :
s ^ m s ^ n
@[simp]
theorem Set.empty_nsmul {α : Type u_1} [inst : ] {n : } (hn : n 0) :
@[simp]
theorem Set.empty_pow {α : Type u_1} [inst : ] {n : } (hn : n 0) :
theorem Set.add_univ_of_zero_mem {α : Type u_1} [inst : ] {s : Set α} (hs : 0 s) :
s + Set.univ = Set.univ
theorem Set.mul_univ_of_one_mem {α : Type u_1} [inst : ] {s : Set α} (hs : 1 s) :
s * Set.univ = Set.univ
theorem Set.univ_add_of_zero_mem {α : Type u_1} [inst : ] {t : Set α} (ht : 0 t) :
Set.univ + t = Set.univ
theorem Set.univ_mul_of_one_mem {α : Type u_1} [inst : ] {t : Set α} (ht : 1 t) :
Set.univ * t = Set.univ
@[simp]
theorem Set.univ_add_univ {α : Type u_1} [inst : ] :
Set.univ + Set.univ = Set.univ
@[simp]
theorem Set.univ_mul_univ {α : Type u_1} [inst : ] :
Set.univ * Set.univ = Set.univ
@[simp]
theorem Set.nsmul_univ {α : Type u_1} [inst : ] {n : } :
n 0n Set.univ = Set.univ
@[simp]
theorem Set.univ_pow {α : Type u_1} [inst : ] {n : } :
n 0Set.univ ^ n = Set.univ
theorem IsAddUnit.set {α : Type u_1} [inst : ] {a : α} :
theorem IsUnit.set {α : Type u_1} [inst : ] {a : α} :
IsUnit {a}
noncomputable def Set.addCommMonoid {α : Type u_1} [inst : ] :

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

Equations
• Set.addCommMonoid = let src := Set.addMonoid; let src_1 := Set.addCommSemigroup; AddCommMonoid.mk (_ : ∀ (a b : Set α), a + b = b + a)
def Set.addCommMonoid.proof_3 {α : Type u_1} [inst : ] (x : Set α) :
= 0
Equations
• (_ : ∀ (x : Set α), = 0) = (_ : ∀ (x : Set α), = 0)
def Set.addCommMonoid.proof_1 {α : Type u_1} [inst : ] (a : Set α) :
0 + a = a
Equations
• (_ : ∀ (a : Set α), 0 + a = a) = (_ : ∀ (a : Set α), 0 + a = a)
def Set.addCommMonoid.proof_4 {α : Type u_1} [inst : ] (n : ) (x : Set α) :
AddMonoid.nsmul (n + 1) x = x +
Equations
def Set.addCommMonoid.proof_5 {α : Type u_1} [inst : ] (a : Set α) (b : Set α) :
a + b = b + a
Equations
• (_ : ∀ (a b : Set α), a + b = b + a) = (_ : ∀ (a b : Set α), a + b = b + a)
def Set.addCommMonoid.proof_2 {α : Type u_1} [inst : ] (a : Set α) :
a + 0 = a
Equations
• (_ : ∀ (a : Set α), a + 0 = a) = (_ : ∀ (a : Set α), a + 0 = a)
noncomputable def Set.commMonoid {α : Type u_1} [inst : ] :

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

Equations
• Set.commMonoid = let src := Set.monoid; let src_1 := Set.commSemigroup; CommMonoid.mk (_ : ∀ (a b : Set α), a * b = b * a)
theorem Set.add_eq_zero_iff {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
s + t = 0 a b, s = {a} t = {b} a + b = 0
theorem Set.mul_eq_one_iff {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
s * t = 1 a b, s = {a} t = {b} a * b = 1
def Set.subtractionMonoid.proof_1 {α : Type u_1} [inst : ] (a : Set α) :
0 + a = a
Equations
• (_ : ∀ (a : Set α), 0 + a = a) = (_ : ∀ (a : Set α), 0 + a = a)
noncomputable def Set.subtractionMonoid {α : Type u_1} [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.
def Set.subtractionMonoid.proof_3 {α : Type u_1} [inst : ] (x : Set α) :
= 0
Equations
• (_ : ∀ (x : Set α), = 0) = (_ : ∀ (x : Set α), = 0)
def Set.subtractionMonoid.proof_5 {α : Type u_1} [inst : ] (s : Set α) (t : Set α) :
s - t = s + -t
Equations
def Set.subtractionMonoid.proof_2 {α : Type u_1} [inst : ] (a : Set α) :
a + 0 = a
Equations
• (_ : ∀ (a : Set α), a + 0 = a) = (_ : ∀ (a : Set α), a + 0 = a)
def Set.subtractionMonoid.proof_10 {α : Type u_1} [inst : ] (x : Set α) :
- -x = x
Equations
• (_ : ∀ (x : Set α), - -x = x) = (_ : ∀ (x : Set α), - -x = x)
def Set.subtractionMonoid.proof_12 {α : Type u_1} [inst : ] (s : Set α) (t : Set α) (h : s + t = 0) :
-s = t
Equations
• (_ : -s = t) = (_ : -s = t)
def Set.subtractionMonoid.proof_6 {α : Type u_1} [inst : ] (a : Set α) (b : Set α) (c : Set α) :
a + b + c = a + (b + c)
Equations
• (_ : ∀ (a b c : Set α), a + b + c = a + (b + c)) = (_ : ∀ (a b c : Set α), a + b + c = a + (b + c))
def Set.subtractionMonoid.proof_8 {α : Type u_1} [inst : ] :
∀ (n : ) (a : Set α), zsmulRec () a = zsmulRec () a
Equations
• (_ : zsmulRec () a = zsmulRec () a) = (_ : zsmulRec () a = zsmulRec () a)
def Set.subtractionMonoid.proof_9 {α : Type u_1} [inst : ] :
∀ (n : ) (a : Set α), zsmulRec () a = zsmulRec () a
Equations
• (_ : zsmulRec () a = zsmulRec () a) = (_ : zsmulRec () a = zsmulRec () a)
def Set.subtractionMonoid.proof_11 {α : Type u_1} [inst : ] (s : Set α) (t : Set α) :
-(s + t) = -t + -s
Equations
def Set.subtractionMonoid.proof_4 {α : Type u_1} [inst : ] (n : ) (x : Set α) :
AddMonoid.nsmul (n + 1) x = x +
Equations
def Set.subtractionMonoid.proof_7 {α : Type u_1} [inst : ] :
∀ (a : Set α), zsmulRec 0 a = zsmulRec 0 a
Equations
• (_ : zsmulRec 0 a = zsmulRec 0 a) = (_ : zsmulRec 0 a = zsmulRec 0 a)
noncomputable def Set.divisionMonoid {α : Type u_1} [inst : ] :

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Set.isAddUnit_iff {α : Type u_1} [inst : ] {s : Set α} :
a, s = {a}
@[simp]
theorem Set.isUnit_iff {α : Type u_1} [inst : ] {s : Set α} :
a, s = {a}
noncomputable def Set.subtractionCommMonoid {α : Type u_1} [inst : ] :

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

Equations
• Set.subtractionCommMonoid = let src := Set.subtractionMonoid; let src_1 := Set.addCommSemigroup; SubtractionCommMonoid.mk (_ : ∀ (a b : Set α), a + b = b + a)
def Set.subtractionCommMonoid.proof_3 {α : Type u_1} [inst : ] (a : Set α) (b : Set α) :
a + b = 0-a = b
Equations
• (_ : ∀ (a b : Set α), a + b = 0-a = b) = (_ : ∀ (a b : Set α), a + b = 0-a = b)
def Set.subtractionCommMonoid.proof_1 {α : Type u_1} [inst : ] (x : Set α) :
- -x = x
Equations
• (_ : ∀ (x : Set α), - -x = x) = (_ : ∀ (x : Set α), - -x = x)
def Set.subtractionCommMonoid.proof_4 {α : Type u_1} [inst : ] (a : Set α) (b : Set α) :
a + b = b + a
Equations
• (_ : ∀ (a b : Set α), a + b = b + a) = (_ : ∀ (a b : Set α), a + b = b + a)
def Set.subtractionCommMonoid.proof_2 {α : Type u_1} [inst : ] (a : Set α) (b : Set α) :
-(a + b) = -b + -a
Equations
noncomputable def Set.divisionCommMonoid {α : Type u_1} [inst : ] :

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

Equations
• Set.divisionCommMonoid = let src := Set.divisionMonoid; let src_1 := Set.commSemigroup; DivisionCommMonoid.mk (_ : ∀ (a b : Set α), a * b = b * a)
noncomputable def Set.hasDistribNeg {α : Type u_1} [inst : Mul α] [inst : ] :

Set α has distributive negation if α has.

Equations
• Set.hasDistribNeg = let src := Set.involutiveNeg; HasDistribNeg.mk (_ : ∀ (x x_1 : Set α), -x * x_1 = -(x * x_1)) (_ : ∀ (x x_1 : Set α), x * -x_1 = -(x * x_1))

Note that Set α is not a Distrib because s * t + s * u has cross terms that s * (t + u) lacks.

theorem Set.mul_add_subset {α : Type u_1} [inst : ] (s : Set α) (t : Set α) (u : Set α) :
s * (t + u) s * t + s * u
theorem Set.add_mul_subset {α : Type u_1} [inst : ] (s : Set α) (t : Set α) (u : Set α) :
(s + t) * u s * u + t * u

Note that Set is not a MulZeroClass because 0 * ∅ ≠ 0∅ ≠ 0≠ 0.

theorem Set.mul_zero_subset {α : Type u_1} [inst : ] (s : Set α) :
s * 0 0
theorem Set.zero_mul_subset {α : Type u_1} [inst : ] (s : Set α) :
0 * s 0
theorem Set.Nonempty.mul_zero {α : Type u_1} [inst : ] {s : Set α} (hs : ) :
s * 0 = 0
theorem Set.Nonempty.zero_mul {α : Type u_1} [inst : ] {s : Set α} (hs : ) :
0 * s = 0

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

@[simp]
theorem Set.zero_mem_sub_iff {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
0 s - t ¬Disjoint s t
@[simp]
theorem Set.one_mem_div_iff {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
1 s / t ¬Disjoint s t
theorem Set.not_zero_mem_sub_iff {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
¬0 s - t Disjoint s t
theorem Set.not_one_mem_div_iff {α : Type u_1} [inst : ] {s : Set α} {t : Set α} :
¬1 s / t Disjoint s t
theorem Disjoint.one_not_mem_div_set {α : Type u_1} [inst : ] {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_1} [inst : ] {s : Set α} {t : Set α} :
Disjoint s t¬0 s - t
abbrev Set.Nonempty.zero_mem_sub.match_1 {α : Type u_1} {s : Set α} (motive : ) :
(h : ) → ((a : α) → (ha : a s) → motive (_ : x, x s)) → motive h
Equations
theorem Set.Nonempty.zero_mem_sub {α : Type u_1} [inst : ] {s : Set α} (h : ) :
0 s - s
theorem Set.Nonempty.one_mem_div {α : Type u_1} [inst : ] {s : Set α} (h : ) :
1 s / s
theorem Set.isAddUnit_singleton {α : Type u_1} [inst : ] (a : α) :
theorem Set.isUnit_singleton {α : Type u_1} [inst : ] (a : α) :
IsUnit {a}
@[simp]
theorem Set.isAddUnit_iff_singleton {α : Type u_1} [inst : ] {s : Set α} :
a, s = {a}
@[simp]
theorem Set.isUnit_iff_singleton {α : Type u_1} [inst : ] {s : Set α} :
a, s = {a}
@[simp]
theorem Set.image_add_left {α : Type u_1} [inst : ] {t : Set α} {a : α} :
(fun x x_1 => x + x_1) a '' t = (fun x x_1 => x + x_1) (-a) ⁻¹' t
@[simp]
theorem Set.image_mul_left {α : Type u_1} [inst : ] {t : Set α} {a : α} :
(fun x x_1 => x * x_1) a '' t = (fun x x_1 => x * x_1) a⁻¹ ⁻¹' t
@[simp]
theorem Set.image_add_right {α : Type u_1} [inst : ] {t : Set α} {b : α} :
(fun x => x + b) '' t = (fun x => x + -b) ⁻¹' t
@[simp]
theorem Set.image_mul_right {α : Type u_1} [inst : ] {t : Set α} {b : α} :
(fun x => x * b) '' t = (fun x => x * b⁻¹) ⁻¹' t
theorem Set.image_add_left' {α : Type u_1} [inst : ] {t : Set α} {a : α} :
(fun b => -a + b) '' t = (fun b => a + b) ⁻¹' t
theorem Set.image_mul_left' {α : Type u_1} [inst : ] {t : Set α} {a : α} :
(fun b => a⁻¹ * b) '' t = (fun b => a * b) ⁻¹' t
theorem Set.image_add_right' {α : Type u_1} [inst : ] {t : Set α} {b : α} :
(fun x => x + -b) '' t = (fun x => x + b) ⁻¹' t
theorem Set.image_mul_right' {α : Type u_1} [inst : ] {t : Set α} {b : α} :
(fun x => x * b⁻¹) '' t = (fun x => x * b) ⁻¹' t
@[simp]
theorem Set.preimage_add_left_singleton {α : Type u_1} [inst : ] {a : α} {b : α} :
(fun x x_1 => x + x_1) a ⁻¹' {b} = {-a + b}
@[simp]
theorem Set.preimage_mul_left_singleton {α : Type u_1} [inst : ] {a : α} {b : α} :
(fun x x_1 => x * x_1) a ⁻¹' {b} = {a⁻¹ * b}
@[simp]
theorem Set.preimage_add_right_singleton {α : Type u_1} [inst : ] {a : α} {b : α} :
(fun x => x + a) ⁻¹' {b} = {b + -a}
@[simp]
theorem Set.preimage_mul_right_singleton {α : Type u_1} [inst : ] {a : α} {b : α} :
(fun x => x * a) ⁻¹' {b} = {b * a⁻¹}
@[simp]
theorem Set.preimage_add_left_zero {α : Type u_1} [inst : ] {a : α} :
(fun x x_1 => x + x_1) a ⁻¹' 0 = {-a}
@[simp]
theorem Set.preimage_mul_left_one {α : Type u_1} [inst : ] {a : α} :
(fun x x_1 => x * x_1) a ⁻¹' 1 = {a⁻¹}
@[simp]
theorem Set.preimage_add_right_zero {α : Type u_1} [inst : ] {b : α} :
(fun x => x + b) ⁻¹' 0 = {-b}
@[simp]
theorem Set.preimage_mul_right_one {α : Type u_1} [inst : ] {b : α} :
(fun x => x * b) ⁻¹' 1 = {b⁻¹}
theorem Set.preimage_add_left_zero' {α : Type u_1} [inst : ] {a : α} :
(fun b => -a + b) ⁻¹' 0 = {a}
theorem Set.preimage_mul_left_one' {α : Type u_1} [inst : ] {a : α} :
(fun b => a⁻¹ * b) ⁻¹' 1 = {a}
theorem Set.preimage_add_right_zero' {α : Type u_1} [inst : ] {b : α} :
(fun x => x + -b) ⁻¹' 0 = {b}
theorem Set.preimage_mul_right_one' {α : Type u_1} [inst : ] {b : α} :
(fun x => x * b⁻¹) ⁻¹' 1 = {b}
@[simp]
theorem Set.add_univ {α : Type u_1} [inst : ] {s : Set α} (hs : ) :
s + Set.univ = Set.univ
@[simp]
theorem Set.mul_univ {α : Type u_1} [inst : ] {s : Set α} (hs : ) :
s * Set.univ = Set.univ
@[simp]
theorem Set.univ_add {α : Type u_1} [inst : ] {t : Set α} (ht : ) :
Set.univ + t = Set.univ
@[simp]
theorem Set.univ_mul {α : Type u_1} [inst : ] {t : Set α} (ht : ) :
Set.univ * t = Set.univ
theorem Set.div_zero_subset {α : Type u_1} [inst : ] (s : Set α) :
s / 0 0
theorem Set.zero_div_subset {α : Type u_1} [inst : ] (s : Set α) :
0 / s 0
theorem Set.Nonempty.div_zero {α : Type u_1} [inst : ] {s : Set α} (hs : ) :
s / 0 = 0
theorem Set.Nonempty.zero_div {α : Type u_1} [inst : ] {s : Set α} (hs : ) :
0 / s = 0
theorem Set.image_add {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Add β] [inst : AddHomClass F α β] (m : F) {s : Set α} {t : Set α} :
m '' (s + t) = m '' s + m '' t
theorem Set.image_mul {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Mul β] [inst : MulHomClass F α β] (m : F) {s : Set α} {t : Set α} :
m '' (s * t) = m '' s * m '' t
theorem Set.preimage_add_preimage_subset {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : Add α] [inst : Add β] [inst : AddHomClass F α β] (m : F) {s : Set β} {t : Set β} :
m ⁻¹' s + m ⁻¹' t m ⁻¹' (s + t)
theorem Set.preimage_mul_preimage_subset {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : Mul α] [inst : Mul β] [inst : MulHomClass F α β] (m : F) {s : Set β} {t : Set β} :
m ⁻¹' s * m ⁻¹' t m ⁻¹' (s * t)
theorem Set.image_sub {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] [inst : ] (m : F) {s : Set α} {t : Set α} :
m '' (s - t) = m '' s - m '' t
theorem Set.image_div {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] [inst : ] (m : F) {s : Set α} {t : Set α} :
m '' (s / t) = m '' s / m '' t
theorem Set.preimage_sub_preimage_subset {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] [inst : ] (m : F) {s : Set β} {t : Set β} :
m ⁻¹' s - m ⁻¹' t m ⁻¹' (s - t)
theorem Set.preimage_div_preimage_subset {F : Type u_3} {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] [inst : ] (m : F) {s : Set β} {t : Set β} :
m ⁻¹' s / m ⁻¹' t m ⁻¹' (s / t)
theorem Set.bddAbove_add {α : Type u_1} [inst : ] {A : Set α} {B : Set α} :
BddAbove (A + B)
theorem Set.bddAbove_mul {α : Type u_1} [inst : ] {A : Set α} {B : Set α} :
BddAbove (A * B)

Miscellaneous #

theorem AddGroup.card_nsmul_eq_card_nsmul_card_univ_aux {f : } (h1 : ) {B : } (h2 : ∀ (n : ), f n B) (h3 : ∀ (n : ), f n = f (n + 1)f (n + 1) = f (n + 2)) (k : ) :
B kf k = f B
theorem Group.card_pow_eq_card_pow_card_univ_aux {f : } (h1 : ) {B : } (h2 : ∀ (n : ), f n B) (h3 : ∀ (n : ), f n = f (n + 1)f (n + 1) = f (n + 2)) (k : ) :
B kf k = f B