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

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 scope `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 scope 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

source
def Mathlib.LibraryNote.«pointwise nat action» :
LibraryNote

Pointwise monoids (`Set`, `Finset`, `Filter`) have derived pointwise actions of the form `SMul α β → SMul α (Set β)`. When `α` is `ℕ` or `ℤ`, this action conflicts with the nat or int action coming from `Set β` being a `Monoid` or `DivInvMonoid`. For example, `2 • {a, b}` can both be `{2 • a, 2 • b}` (pointwise action, pointwise repeated addition, `Set.smulSet`) and `{a + a, a + b, b + a, b + b}` (nat or int action, repeated pointwise addition, `Set.NSMul`).

Because the pointwise action can easily be spelled out in such cases, we give higher priority to the nat and int actions.

Equations

- Mathlib.LibraryNote.«pointwise nat action» = ()

Instances For

### `0`/`1` as sets #

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

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

Equations

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

Instances For

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

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

Equations

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

Instances For

source
theorem Set.singleton_one {α : Type u_2} [One α] :
{1} = 1
source
theorem Set.singleton_zero {α : Type u_2} [Zero α] :
{0} = 0
source
@[simp]
theorem Set.mem_one {α : Type u_2} [One α] {a : α} :
a ∈ 1 ↔ a = 1
source
@[simp]
theorem Set.mem_zero {α : Type u_2} [Zero α] {a : α} :
a ∈ 0 ↔ a = 0
source
theorem Set.one_mem_one {α : Type u_2} [One α] :
1 ∈ 1
source
theorem Set.zero_mem_zero {α : Type u_2} [Zero α] :
0 ∈ 0
source
@[simp]
theorem Set.one_subset {α : Type u_2} [One α] {s : Set α} :
1 ⊆ s ↔ 1 ∈ s
source
@[simp]
theorem Set.zero_subset {α : Type u_2} [Zero α] {s : Set α} :
0 ⊆ s ↔ 0 ∈ s
source
@[simp]
theorem Set.one_nonempty {α : Type u_2} [One α] :
Set.Nonempty 1
source
@[simp]
theorem Set.zero_nonempty {α : Type u_2} [Zero α] :
Set.Nonempty 0
source
@[simp]
theorem Set.image_one {α : Type u_2} {β : Type u_3} [One α] {f : α → β} :
f '' 1 = {f 1}
source
@[simp]
theorem Set.image_zero {α : Type u_2} {β : Type u_3} [Zero α] {f : α → β} :
f '' 0 = {f 0}
source
theorem Set.subset_one_iff_eq {α : Type u_2} [One α] {s : Set α} :
s ⊆ 1 ↔ s = ∅ ∨ s = 1
source
theorem Set.subset_zero_iff_eq {α : Type u_2} [Zero α] {s : Set α} :
s ⊆ 0 ↔ s = ∅ ∨ s = 0
source
theorem Set.Nonempty.subset_one_iff {α : Type u_2} [One α] {s : Set α} (h : s.Nonempty) :
s ⊆ 1 ↔ s = 1
source
theorem Set.Nonempty.subset_zero_iff {α : Type u_2} [Zero α] {s : Set α} (h : s.Nonempty) :
s ⊆ 0 ↔ s = 0
source
def Set.singletonOneHom {α : Type u_2} [One α] :
OneHom α (Set α)

The singleton operation as a `OneHom`.

Equations

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

Instances For

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

The singleton operation as a `ZeroHom`.

Equations

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

Instances For

source
@[simp]
theorem Set.coe_singletonOneHom {α : Type u_2} [One α] :
⇑singletonOneHom = singleton
source
@[simp]
theorem Set.coe_singletonZeroHom {α : Type u_2} [Zero α] :
⇑singletonZeroHom = singleton
source
theorem Set.image_op_one {α : Type u_2} [One α] :
MulOpposite.op '' 1 = 1
source
theorem Set.image_op_zero {α : Type u_2} [Zero α] :
AddOpposite.op '' 0 = 0
source
@[simp]
theorem Set.one_prod_one {α : Type u_2} {β : Type u_3} [One α] [One β] :
1 ×ˢ 1 = 1
source
@[simp]
theorem Set.zero_prod_zero {α : Type u_2} {β : Type u_3} [Zero α] [Zero β] :
0 ×ˢ 0 = 0

### Set negation/inversion #

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

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

Equations

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

Instances For

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

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

Equations

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

Instances For

source
@[simp]
theorem Set.inv_setOf {α : Type u_2} [Inv α] (p : α → Prop) :
{x : α | p x}⁻¹ = {x : α | p x⁻¹}
source
@[simp]
theorem Set.neg_setOf {α : Type u_2} [Neg α] (p : α → Prop) :
-{x : α | p x} = {x : α | p (-x)}
source
@[simp]
theorem Set.mem_inv {α : Type u_2} [Inv α] {s : Set α} {a : α} :
a ∈ s⁻¹ ↔ a⁻¹ ∈ s
source
@[simp]
theorem Set.mem_neg {α : Type u_2} [Neg α] {s : Set α} {a : α} :
a ∈ -s ↔ -a ∈ s
source
@[simp]
theorem Set.inv_preimage {α : Type u_2} [Inv α] {s : Set α} :
Inv.inv ⁻¹' s = s⁻¹
source
@[simp]
theorem Set.neg_preimage {α : Type u_2} [Neg α] {s : Set α} :
Neg.neg ⁻¹' s = -s
source
@[simp]
theorem Set.inv_empty {α : Type u_2} [Inv α] :
∅⁻¹ = ∅
source
@[simp]
theorem Set.neg_empty {α : Type u_2} [Neg α] :
-∅ = ∅
source
@[simp]
theorem Set.inv_univ {α : Type u_2} [Inv α] :
univ⁻¹ = univ
source
@[simp]
theorem Set.neg_univ {α : Type u_2} [Neg α] :
-univ = univ
source
@[simp]
theorem Set.inter_inv {α : Type u_2} [Inv α] {s t : Set α} :
(s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹
source
@[simp]
theorem Set.inter_neg {α : Type u_2} [Neg α] {s t : Set α} :
-(s ∩ t) = -s ∩ -t
source
@[simp]
theorem Set.union_inv {α : Type u_2} [Inv α] {s t : Set α} :
(s ∪ t)⁻¹ = s⁻¹ ∪ t⁻¹
source
@[simp]
theorem Set.union_neg {α : Type u_2} [Neg α] {s t : Set α} :
-(s ∪ t) = -s ∪ -t
source
@[simp]
theorem Set.compl_inv {α : Type u_2} [Inv α] {s : Set α} :
s ᶜ⁻¹ = s⁻¹ ᶜ
source
@[simp]
theorem Set.compl_neg {α : Type u_2} [Neg α] {s : Set α} :
-s ᶜ = (-s)ᶜ
source
@[simp]
theorem Set.inv_prod {α : Type u_2} {β : Type u_3} [Inv α] [Inv β] (s : Set α) (t : Set β) :
(s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹
source
@[simp]
theorem Set.neg_prod {α : Type u_2} {β : Type u_3} [Neg α] [Neg β] (s : Set α) (t : Set β) :
-s ×ˢ t = (-s) ×ˢ (-t)
source
theorem Set.inv_mem_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} {a : α} :
a⁻¹ ∈ s⁻¹ ↔ a ∈ s
source
theorem Set.neg_mem_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} {a : α} :
-a ∈ -s ↔ a ∈ s
source
@[simp]
theorem Set.nonempty_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
s⁻¹.Nonempty ↔ s.Nonempty
source
@[simp]
theorem Set.nonempty_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
(-s).Nonempty ↔ s.Nonempty
source
theorem Set.Nonempty.inv {α : Type u_2} [InvolutiveInv α] {s : Set α} (h : s.Nonempty) :
s⁻¹.Nonempty
source
theorem Set.Nonempty.neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} (h : s.Nonempty) :
(-s).Nonempty
source
@[simp]
theorem Set.image_inv_eq_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
(fun (x : α) => x⁻¹) '' s = s⁻¹
source
@[simp]
theorem Set.image_neg_eq_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
(fun (x : α) => -x) '' s = -s
source
@[simp]
theorem Set.inv_eq_empty {α : Type u_2} [InvolutiveInv α] {s : Set α} :
s⁻¹ = ∅ ↔ s = ∅
source
@[simp]
theorem Set.neg_eq_empty {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
-s = ∅ ↔ s = ∅
source
instance Set.involutiveInv {α : Type u_2} [InvolutiveInv α] :
InvolutiveInv (Set α)
Equations

- Set.involutiveInv = { toInv := Set.inv, inv_inv := ⋯ }

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

- Set.involutiveNeg = { toNeg := Set.neg, neg_neg := ⋯ }

source
@[simp]
theorem Set.inv_subset_inv {α : Type u_2} [InvolutiveInv α] {s t : Set α} :
s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t
source
@[simp]
theorem Set.neg_subset_neg {α : Type u_2} [InvolutiveNeg α] {s t : Set α} :
-s ⊆ -t ↔ s ⊆ t
source
theorem Set.inv_subset {α : Type u_2} [InvolutiveInv α] {s t : Set α} :
s⁻¹ ⊆ t ↔ s ⊆ t⁻¹
source
theorem Set.neg_subset {α : Type u_2} [InvolutiveNeg α] {s t : Set α} :
-s ⊆ t ↔ s ⊆ -t
source
@[simp]
theorem Set.inv_singleton {α : Type u_2} [InvolutiveInv α] (a : α) :
{a}⁻¹ = {a⁻¹}
source
@[simp]
theorem Set.neg_singleton {α : Type u_2} [InvolutiveNeg α] (a : α) :
-{a} = {-a}
source
@[simp]
theorem Set.inv_insert {α : Type u_2} [InvolutiveInv α] (a : α) (s : Set α) :
(insert a s)⁻¹ = insert a⁻¹ s⁻¹
source
@[simp]
theorem Set.neg_insert {α : Type u_2} [InvolutiveNeg α] (a : α) (s : Set α) :
-insert a s = insert (-a) (-s)
source
theorem Set.inv_range {α : Type u_2} [InvolutiveInv α] {ι : Sort u_5} {f : ι → α} :
(range f)⁻¹ = range fun (i : ι) => (f i)⁻¹
source
theorem Set.neg_range {α : Type u_2} [InvolutiveNeg α] {ι : Sort u_5} {f : ι → α} :
-range f = range fun (i : ι) => -f i
source
theorem Set.image_op_inv {α : Type u_2} [InvolutiveInv α] {s : Set α} :
MulOpposite.op '' s⁻¹ = (MulOpposite.op '' s)⁻¹
source
theorem Set.image_op_neg {α : Type u_2} [InvolutiveNeg α] {s : Set α} :
AddOpposite.op '' (-s) = -AddOpposite.op '' s

### Set addition/multiplication #

source
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 scope `Pointwise`.

Equations

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

Instances For

source
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 }

Instances For

source
@[simp]
theorem Set.image2_mul {α : Type u_2} [Mul α] {s t : Set α} :
image2 (fun (x1 x2 : α) => x1 * x2) s t = s * t
source
@[simp]
theorem Set.image2_add {α : Type u_2} [Add α] {s t : Set α} :
image2 (fun (x1 x2 : α) => x1 + x2) s t = s + t
source
theorem Set.mem_mul {α : Type u_2} [Mul α] {s t : Set α} {a : α} :
a ∈ s * t ↔ ∃ x ∈ s, ∃ y ∈ t, x * y = a
source
theorem Set.mem_add {α : Type u_2} [Add α] {s t : Set α} {a : α} :
a ∈ s + t ↔ ∃ x ∈ s, ∃ y ∈ t, x + y = a
source
theorem Set.mul_mem_mul {α : Type u_2} [Mul α] {s t : Set α} {a b : α} :
a ∈ s → b ∈ t → a * b ∈ s * t
source
theorem Set.add_mem_add {α : Type u_2} [Add α] {s t : Set α} {a b : α} :
a ∈ s → b ∈ t → a + b ∈ s + t
source
theorem Set.image_mul_prod {α : Type u_2} [Mul α] {s t : Set α} :
(fun (x : α × α) => x.1 * x.2) '' s ×ˢ t = s * t
source
theorem Set.add_image_prod {α : Type u_2} [Add α] {s t : Set α} :
(fun (x : α × α) => x.1 + x.2) '' s ×ˢ t = s + t
source
@[simp]
theorem Set.empty_mul {α : Type u_2} [Mul α] {s : Set α} :
∅ * s = ∅
source
@[simp]
theorem Set.empty_add {α : Type u_2} [Add α] {s : Set α} :
∅ + s = ∅
source
@[simp]
theorem Set.mul_empty {α : Type u_2} [Mul α] {s : Set α} :
s * ∅ = ∅
source
@[simp]
theorem Set.add_empty {α : Type u_2} [Add α] {s : Set α} :
s + ∅ = ∅
source
@[simp]
theorem Set.mul_eq_empty {α : Type u_2} [Mul α] {s t : Set α} :
s * t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem Set.add_eq_empty {α : Type u_2} [Add α] {s t : Set α} :
s + t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem Set.mul_nonempty {α : Type u_2} [Mul α] {s t : Set α} :
(s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
source
@[simp]
theorem Set.add_nonempty {α : Type u_2} [Add α] {s t : Set α} :
(s + t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
source
theorem Set.Nonempty.mul {α : Type u_2} [Mul α] {s t : Set α} :
s.Nonempty → t.Nonempty → (s * t).Nonempty
source
theorem Set.Nonempty.add {α : Type u_2} [Add α] {s t : Set α} :
s.Nonempty → t.Nonempty → (s + t).Nonempty
source
theorem Set.Nonempty.of_mul_left {α : Type u_2} [Mul α] {s t : Set α} :
(s * t).Nonempty → s.Nonempty
source
theorem Set.Nonempty.of_add_left {α : Type u_2} [Add α] {s t : Set α} :
(s + t).Nonempty → s.Nonempty
source
theorem Set.Nonempty.of_mul_right {α : Type u_2} [Mul α] {s t : Set α} :
(s * t).Nonempty → t.Nonempty
source
theorem Set.Nonempty.of_add_right {α : Type u_2} [Add α] {s t : Set α} :
(s + t).Nonempty → t.Nonempty
source
@[simp]
theorem Set.mul_singleton {α : Type u_2} [Mul α] {s : Set α} {b : α} :
s * {b} = (fun (x : α) => x * b) '' s
source
@[simp]
theorem Set.add_singleton {α : Type u_2} [Add α] {s : Set α} {b : α} :
s + {b} = (fun (x : α) => x + b) '' s
source
@[simp]
theorem Set.singleton_mul {α : Type u_2} [Mul α] {t : Set α} {a : α} :
{a} * t = (fun (x : α) => a * x) '' t
source
@[simp]
theorem Set.singleton_add {α : Type u_2} [Add α] {t : Set α} {a : α} :
{a} + t = (fun (x : α) => a + x) '' t
source
theorem Set.singleton_mul_singleton {α : Type u_2} [Mul α] {a b : α} :
{a} * {b} = {a * b}
source
theorem Set.singleton_add_singleton {α : Type u_2} [Add α] {a b : α} :
{a} + {b} = {a + b}
source
theorem Set.mul_subset_mul {α : Type u_2} [Mul α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ * s₂ ⊆ t₁ * t₂
source
theorem Set.add_subset_add {α : Type u_2} [Add α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ + s₂ ⊆ t₁ + t₂
source
theorem Set.mul_subset_mul_left {α : Type u_2} [Mul α] {s t₁ t₂ : Set α} :
t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂
source
theorem Set.add_subset_add_left {α : Type u_2} [Add α] {s t₁ t₂ : Set α} :
t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂
source
theorem Set.mul_subset_mul_right {α : Type u_2} [Mul α] {s₁ s₂ t : Set α} :
s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t
source
theorem Set.add_subset_add_right {α : Type u_2} [Add α] {s₁ s₂ t : Set α} :
s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t
source
instance Set.instMulLeftMono {α : Type u_2} [Mul α] :
MulLeftMono (Set α)
source
instance Set.instAddLeftMono {α : Type u_2} [Add α] :
AddLeftMono (Set α)
source
instance Set.instMulRightMono {α : Type u_2} [Mul α] :
MulRightMono (Set α)
source
instance Set.instAddRightMono {α : Type u_2} [Add α] :
AddRightMono (Set α)
source
theorem Set.mul_subset_iff {α : Type u_2} [Mul α] {s t u : Set α} :
s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u
source
theorem Set.add_subset_iff {α : Type u_2} [Add α] {s t u : Set α} :
s + t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ u
source
theorem Set.union_mul {α : Type u_2} [Mul α] {s₁ s₂ t : Set α} :
(s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t
source
theorem Set.union_add {α : Type u_2} [Add α] {s₁ s₂ t : Set α} :
s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)
source
theorem Set.mul_union {α : Type u_2} [Mul α] {s t₁ t₂ : Set α} :
s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂
source
theorem Set.add_union {α : Type u_2} [Add α] {s t₁ t₂ : Set α} :
s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)
source
theorem Set.inter_mul_subset {α : Type u_2} [Mul α] {s₁ s₂ t : Set α} :
s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)
source
theorem Set.inter_add_subset {α : Type u_2} [Add α] {s₁ s₂ t : Set α} :
s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)
source
theorem Set.mul_inter_subset {α : Type u_2} [Mul α] {s t₁ t₂ : Set α} :
s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)
source
theorem Set.add_inter_subset {α : Type u_2} [Add α] {s t₁ t₂ : Set α} :
s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)
source
theorem Set.inter_mul_union_subset_union {α : Type u_2} [Mul α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
source
theorem Set.inter_add_union_subset_union {α : Type u_2} [Add α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)
source
theorem Set.union_mul_inter_subset_union {α : Type u_2} [Mul α] {s₁ s₂ t₁ t₂ : Set α} :
(s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
source
theorem Set.union_add_inter_subset_union {α : Type u_2} [Add α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)
source
def Set.singletonMulHom {α : Type u_2} [Mul α] :
α →ₙ* Set α

The singleton operation as a `MulHom`.

Equations

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

Instances For

source
def Set.singletonAddHom {α : Type u_2} [Add α] :
α →ₙ+ Set α

The singleton operation as an `AddHom`.

Equations

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

Instances For

source
@[simp]
theorem Set.coe_singletonMulHom {α : Type u_2} [Mul α] :
⇑singletonMulHom = singleton
source
@[simp]
theorem Set.coe_singletonAddHom {α : Type u_2} [Add α] :
⇑singletonAddHom = singleton
source
@[simp]
theorem Set.singletonMulHom_apply {α : Type u_2} [Mul α] (a : α) :
singletonMulHom a = {a}
source
@[simp]
theorem Set.singletonAddHom_apply {α : Type u_2} [Add α] (a : α) :
singletonAddHom a = {a}
source
@[simp]
theorem Set.image_op_mul {α : Type u_2} [Mul α] {s t : Set α} :
MulOpposite.op '' (s * t) = MulOpposite.op '' t * MulOpposite.op '' s
source
@[simp]
theorem Set.image_op_add {α : Type u_2} [Add α] {s t : Set α} :
AddOpposite.op '' (s + t) = AddOpposite.op '' t + AddOpposite.op '' s
source
@[simp]
theorem Set.prod_mul_prod_comm {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (s₁ s₂ : Set α) (t₁ t₂ : Set β) :
s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)
source
@[simp]
theorem Set.prod_add_prod_comm {α : Type u_2} {β : Type u_3} [Add α] [Add β] (s₁ s₂ : Set α) (t₁ t₂ : Set β) :
s₁ ×ˢ t₁ + s₂ ×ˢ t₂ = (s₁ + s₂) ×ˢ (t₁ + t₂)

### Set subtraction/division #

source
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 }

Instances For

source
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 }

Instances For

source
@[simp]
theorem Set.image2_div {α : Type u_2} [Div α] {s t : Set α} :
image2 (fun (x1 x2 : α) => x1 / x2) s t = s / t
source
@[simp]
theorem Set.image2_sub {α : Type u_2} [Sub α] {s t : Set α} :
image2 (fun (x1 x2 : α) => x1 - x2) s t = s - t
source
theorem Set.mem_div {α : Type u_2} [Div α] {s t : Set α} {a : α} :
a ∈ s / t ↔ ∃ x ∈ s, ∃ y ∈ t, x / y = a
source
theorem Set.mem_sub {α : Type u_2} [Sub α] {s t : Set α} {a : α} :
a ∈ s - t ↔ ∃ x ∈ s, ∃ y ∈ t, x - y = a
source
theorem Set.div_mem_div {α : Type u_2} [Div α] {s t : Set α} {a b : α} :
a ∈ s → b ∈ t → a / b ∈ s / t
source
theorem Set.sub_mem_sub {α : Type u_2} [Sub α] {s t : Set α} {a b : α} :
a ∈ s → b ∈ t → a - b ∈ s - t
source
theorem Set.image_div_prod {α : Type u_2} [Div α] {s t : Set α} :
(fun (x : α × α) => x.1 / x.2) '' s ×ˢ t = s / t
source
theorem Set.sub_image_prod {α : Type u_2} [Sub α] {s t : Set α} :
(fun (x : α × α) => x.1 - x.2) '' s ×ˢ t = s - t
source
@[simp]
theorem Set.empty_div {α : Type u_2} [Div α] {s : Set α} :
∅ / s = ∅
source
@[simp]
theorem Set.empty_sub {α : Type u_2} [Sub α] {s : Set α} :
∅ - s = ∅
source
@[simp]
theorem Set.div_empty {α : Type u_2} [Div α] {s : Set α} :
s / ∅ = ∅
source
@[simp]
theorem Set.sub_empty {α : Type u_2} [Sub α] {s : Set α} :
s - ∅ = ∅
source
@[simp]
theorem Set.div_eq_empty {α : Type u_2} [Div α] {s t : Set α} :
s / t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem Set.sub_eq_empty {α : Type u_2} [Sub α] {s t : Set α} :
s - t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem Set.div_nonempty {α : Type u_2} [Div α] {s t : Set α} :
(s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
source
@[simp]
theorem Set.sub_nonempty {α : Type u_2} [Sub α] {s t : Set α} :
(s - t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
source
theorem Set.Nonempty.div {α : Type u_2} [Div α] {s t : Set α} :
s.Nonempty → t.Nonempty → (s / t).Nonempty
source
theorem Set.Nonempty.sub {α : Type u_2} [Sub α] {s t : Set α} :
s.Nonempty → t.Nonempty → (s - t).Nonempty
source
theorem Set.Nonempty.of_div_left {α : Type u_2} [Div α] {s t : Set α} :
(s / t).Nonempty → s.Nonempty
source
theorem Set.Nonempty.of_sub_left {α : Type u_2} [Sub α] {s t : Set α} :
(s - t).Nonempty → s.Nonempty
source
theorem Set.Nonempty.of_div_right {α : Type u_2} [Div α] {s t : Set α} :
(s / t).Nonempty → t.Nonempty
source
theorem Set.Nonempty.of_sub_right {α : Type u_2} [Sub α] {s t : Set α} :
(s - t).Nonempty → t.Nonempty
source
@[simp]
theorem Set.div_singleton {α : Type u_2} [Div α] {s : Set α} {b : α} :
s / {b} = (fun (x : α) => x / b) '' s
source
@[simp]
theorem Set.sub_singleton {α : Type u_2} [Sub α] {s : Set α} {b : α} :
s - {b} = (fun (x : α) => x - b) '' s
source
@[simp]
theorem Set.singleton_div {α : Type u_2} [Div α] {t : Set α} {a : α} :
{a} / t = (fun (x1 x2 : α) => x1 / x2) a '' t
source
@[simp]
theorem Set.singleton_sub {α : Type u_2} [Sub α] {t : Set α} {a : α} :
{a} - t = (fun (x1 x2 : α) => x1 - x2) a '' t
source
theorem Set.singleton_div_singleton {α : Type u_2} [Div α] {a b : α} :
{a} / {b} = {a / b}
source
theorem Set.singleton_sub_singleton {α : Type u_2} [Sub α] {a b : α} :
{a} - {b} = {a - b}
source
theorem Set.div_subset_div {α : Type u_2} [Div α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ / s₂ ⊆ t₁ / t₂
source
theorem Set.sub_subset_sub {α : Type u_2} [Sub α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ - s₂ ⊆ t₁ - t₂
source
theorem Set.div_subset_div_left {α : Type u_2} [Div α] {s t₁ t₂ : Set α} :
t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂
source
theorem Set.sub_subset_sub_left {α : Type u_2} [Sub α] {s t₁ t₂ : Set α} :
t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂
source
theorem Set.div_subset_div_right {α : Type u_2} [Div α] {s₁ s₂ t : Set α} :
s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t
source
theorem Set.sub_subset_sub_right {α : Type u_2} [Sub α] {s₁ s₂ t : Set α} :
s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t
source
theorem Set.div_subset_iff {α : Type u_2} [Div α] {s t u : Set α} :
s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u
source
theorem Set.sub_subset_iff {α : Type u_2} [Sub α] {s t u : Set α} :
s - t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x - y ∈ u
source
theorem Set.union_div {α : Type u_2} [Div α] {s₁ s₂ t : Set α} :
(s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t
source
theorem Set.union_sub {α : Type u_2} [Sub α] {s₁ s₂ t : Set α} :
s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)
source
theorem Set.div_union {α : Type u_2} [Div α] {s t₁ t₂ : Set α} :
s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂
source
theorem Set.sub_union {α : Type u_2} [Sub α] {s t₁ t₂ : Set α} :
s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)
source
theorem Set.inter_div_subset {α : Type u_2} [Div α] {s₁ s₂ t : Set α} :
s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)
source
theorem Set.inter_sub_subset {α : Type u_2} [Sub α] {s₁ s₂ t : Set α} :
s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)
source
theorem Set.div_inter_subset {α : Type u_2} [Div α] {s t₁ t₂ : Set α} :
s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)
source
theorem Set.sub_inter_subset {α : Type u_2} [Sub α] {s t₁ t₂ : Set α} :
s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)
source
theorem Set.inter_div_union_subset_union {α : Type u_2} [Div α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
source
theorem Set.inter_sub_union_subset_union {α : Type u_2} [Sub α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)
source
theorem Set.union_div_inter_subset_union {α : Type u_2} [Div α] {s₁ s₂ t₁ t₂ : Set α} :
(s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
source
theorem Set.union_sub_inter_subset_union {α : Type u_2} [Sub α] {s₁ s₂ t₁ t₂ : Set α} :
s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)
source
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 }

Instances For

source
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 }

Instances For

source
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 }

Instances For

source
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 }

Instances For

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

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

Equations

- Set.semigroup = { toMul := Set.mul, mul_assoc := ⋯ }

Instances For

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

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

Equations

- Set.addSemigroup = { toAdd := Set.add, add_assoc := ⋯ }

Instances For

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

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

Equations

- Set.commSemigroup = { toSemigroup := Set.semigroup, mul_comm := ⋯ }

Instances For

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

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

Equations

- Set.addCommSemigroup = { toAddSemigroup := Set.addSemigroup, add_comm := ⋯ }

Instances For

source
theorem Set.inter_mul_union_subset {α : Type u_2} [CommSemigroup α] {s t : Set α} :
s ∩ t * (s ∪ t) ⊆ s * t
source
theorem Set.inter_add_union_subset {α : Type u_2} [AddCommSemigroup α] {s t : Set α} :
s ∩ t + (s ∪ t) ⊆ s + t
source
theorem Set.union_mul_inter_subset {α : Type u_2} [CommSemigroup α] {s t : Set α} :
(s ∪ t) * (s ∩ t) ⊆ s * t
source
theorem Set.union_add_inter_subset {α : Type u_2} [AddCommSemigroup α] {s t : Set α} :
s ∪ t + s ∩ t ⊆ s + t
source
def Set.mulOneClass {α : Type u_2} [MulOneClass α] :
MulOneClass (Set α)

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

Equations

- Set.mulOneClass = { toOne := Set.one, toMul := Set.mul, one_mul := ⋯, mul_one := ⋯ }

Instances For

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

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

Equations

- Set.addZeroClass = { toZero := Set.zero, toAdd := Set.add, zero_add := ⋯, add_zero := ⋯ }

Instances For

source
theorem Set.subset_mul_left {α : Type u_2} [MulOneClass α] (s : Set α) {t : Set α} (ht : 1 ∈ t) :
s ⊆ s * t
source
theorem Set.subset_add_left {α : Type u_2} [AddZeroClass α] (s : Set α) {t : Set α} (ht : 0 ∈ t) :
s ⊆ s + t
source
theorem Set.subset_mul_right {α : Type u_2} [MulOneClass α] {s : Set α} (t : Set α) (hs : 1 ∈ s) :
t ⊆ s * t
source
theorem Set.subset_add_right {α : Type u_2} [AddZeroClass α] {s : Set α} (t : Set α) (hs : 0 ∈ s) :
t ⊆ s + t
source
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' := ⋯ }

Instances For

source
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' := ⋯ }

Instances For

source
@[simp]
theorem Set.coe_singletonMonoidHom {α : Type u_2} [MulOneClass α] :
⇑singletonMonoidHom = singleton
source
@[simp]
theorem Set.coe_singletonAddMonoidHom {α : Type u_2} [AddZeroClass α] :
⇑singletonAddMonoidHom = singleton
source
@[simp]
theorem Set.singletonMonoidHom_apply {α : Type u_2} [MulOneClass α] (a : α) :
singletonMonoidHom a = {a}
source
@[simp]
theorem Set.singletonAddMonoidHom_apply {α : Type u_2} [AddZeroClass α] (a : α) :
singletonAddMonoidHom a = {a}
source
def Set.monoid {α : Type u_2} [Monoid α] :
Monoid (Set α)

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

Equations

- Set.monoid = { toSemigroup := Set.semigroup, toOne := Set.mulOneClass.toOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

Instances For

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

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

Equations

- Set.addMonoid = { toAddSemigroup := Set.addSemigroup, toZero := Set.addZeroClass.toZero, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯ }

Instances For

source
theorem Set.pow_right_monotone {α : Type u_2} [Monoid α] {s : Set α} (hs : 1 ∈ s) :
Monotone fun (x : ℕ) => s ^ x
source
theorem Set.nsmul_right_monotone {α : Type u_2} [AddMonoid α] {s : Set α} (hs : 0 ∈ s) :
Monotone fun (x : ℕ) => x • s
source
theorem Set.pow_subset_pow_left {α : Type u_2} [Monoid α] {s t : Set α} {n : ℕ} (hst : s ⊆ t) :
s ^ n ⊆ t ^ n
source
theorem Set.nsmul_subset_nsmul_left {α : Type u_2} [AddMonoid α] {s t : Set α} {n : ℕ} (hst : s ⊆ t) :
n • s ⊆ n • t
source
theorem Set.pow_subset_pow_right {α : Type u_2} [Monoid α] {s : Set α} {m n : ℕ} (hs : 1 ∈ s) (hmn : m ≤ n) :
s ^ m ⊆ s ^ n
source
theorem Set.nsmul_subset_nsmul_right {α : Type u_2} [AddMonoid α] {s : Set α} {m n : ℕ} (hs : 0 ∈ s) (hmn : m ≤ n) :
m • s ⊆ n • s
source
theorem Set.pow_subset_pow {α : Type u_2} [Monoid α] {s t : Set α} {m n : ℕ} (hst : s ⊆ t) (ht : 1 ∈ t) (hmn : m ≤ n) :
s ^ m ⊆ t ^ n
source
theorem Set.nsmul_subset_nsmul {α : Type u_2} [AddMonoid α] {s t : Set α} {m n : ℕ} (hst : s ⊆ t) (ht : 0 ∈ t) (hmn : m ≤ n) :
m • s ⊆ n • t
source
theorem Set.subset_pow {α : Type u_2} [Monoid α] {s : Set α} {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) :
s ⊆ s ^ n
source
theorem Set.subset_nsmul {α : Type u_2} [AddMonoid α] {s : Set α} {n : ℕ} (hs : 0 ∈ s) (hn : n ≠ 0) :
s ⊆ n • s
source
theorem Set.pow_subset_pow_mul_of_sq_subset_mul {α : Type u_2} [Monoid α] {s t : Set α} {n : ℕ} (hst : s ^ 2 ⊆ t * s) (hn : n ≠ 0) :
s ^ n ⊆ t ^ (n - 1) * s
source
theorem Set.nsmul_subset_nsmul_add_of_sq_subset_add {α : Type u_2} [AddMonoid α] {s t : Set α} {n : ℕ} (hst : 2 • s ⊆ t + s) (hn : n ≠ 0) :
n • s ⊆ (n - 1) • t + s
source
@[simp]
theorem Set.empty_pow {α : Type u_2} [Monoid α] {n : ℕ} (hn : n ≠ 0) :
∅ ^ n = ∅
source
@[simp]
theorem Set.nsmul_empty {α : Type u_2} [AddMonoid α] {n : ℕ} (hn : n ≠ 0) :
n • ∅ = ∅
source
theorem Set.Nonempty.pow {α : Type u_2} [Monoid α] {s : Set α} (hs : s.Nonempty) {n : ℕ} :
(s ^ n).Nonempty
source
theorem Set.Nonempty.nsmul {α : Type u_2} [AddMonoid α] {s : Set α} (hs : s.Nonempty) {n : ℕ} :
(n • s).Nonempty
source
@[simp]
theorem Set.pow_eq_empty {α : Type u_2} [Monoid α] {s : Set α} {n : ℕ} :
s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
source
@[simp]
theorem Set.nsmul_eq_empty {α : Type u_2} [AddMonoid α] {s : Set α} {n : ℕ} :
n • s = ∅ ↔ s = ∅ ∧ n ≠ 0
source
@[simp]
theorem Set.singleton_pow {α : Type u_2} [Monoid α] (a : α) (n : ℕ) :
{a} ^ n = {a ^ n}
source
@[simp]
theorem Set.nsmul_singleton {α : Type u_2} [AddMonoid α] (a : α) (n : ℕ) :
n • {a} = {n • a}
source
theorem Set.pow_mem_pow {α : Type u_2} [Monoid α] {s : Set α} {a : α} {n : ℕ} (ha : a ∈ s) :
a ^ n ∈ s ^ n
source
theorem Set.nsmul_mem_nsmul {α : Type u_2} [AddMonoid α] {s : Set α} {a : α} {n : ℕ} (ha : a ∈ s) :
n • a ∈ n • s
source
theorem Set.one_mem_pow {α : Type u_2} [Monoid α] {s : Set α} {n : ℕ} (hs : 1 ∈ s) :
1 ∈ s ^ n
source
theorem Set.zero_mem_nsmul {α : Type u_2} [AddMonoid α] {s : Set α} {n : ℕ} (hs : 0 ∈ s) :
0 ∈ n • s
source
theorem Set.inter_pow_subset {α : Type u_2} [Monoid α] {s t : Set α} {n : ℕ} :
(s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n
source
theorem Set.inter_nsmul_subset {α : Type u_2} [AddMonoid α] {s t : Set α} {n : ℕ} :
n • (s ∩ t) ⊆ n • s ∩ n • t
source
theorem Set.mul_univ_of_one_mem {α : Type u_2} [Monoid α] {s : Set α} (hs : 1 ∈ s) :
s * univ = univ
source
theorem Set.add_univ_of_zero_mem {α : Type u_2} [AddMonoid α] {s : Set α} (hs : 0 ∈ s) :
s + univ = univ
source
theorem Set.univ_mul_of_one_mem {α : Type u_2} [Monoid α] {t : Set α} (ht : 1 ∈ t) :
univ * t = univ
source
theorem Set.univ_add_of_zero_mem {α : Type u_2} [AddMonoid α] {t : Set α} (ht : 0 ∈ t) :
univ + t = univ
source
@[simp]
theorem Set.univ_mul_univ {α : Type u_2} [Monoid α] :
univ * univ = univ
source
@[simp]
theorem Set.univ_add_univ {α : Type u_2} [AddMonoid α] :
univ + univ = univ
source
@[simp]
theorem Set.univ_pow {α : Type u_2} [Monoid α] {n : ℕ} :
n ≠ 0 → univ ^ n = univ
source
@[simp]
theorem Set.nsmul_univ {α : Type u_2} [AddMonoid α] {n : ℕ} :
n ≠ 0 → n • univ = univ
source
theorem IsUnit.set {α : Type u_2} [Monoid α] {a : α} :
IsUnit a → IsUnit {a}
source
theorem IsAddUnit.set {α : Type u_2} [AddMonoid α] {a : α} :
IsAddUnit a → IsAddUnit {a}
source
theorem Set.prod_pow {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] (s : Set α) (t : Set β) (n : ℕ) :
s ×ˢ t ^ n = (s ^ n) ×ˢ (t ^ n)
source
theorem Set.nsmul_prod {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddMonoid β] (s : Set α) (t : Set β) (n : ℕ) :
n • s ×ˢ t = (n • s) ×ˢ (n • t)
source
theorem Set.Nontrivial.mul_left {α : Type u_2} [Mul α] [IsLeftCancelMul α] {s t : Set α} :
t.Nontrivial → s.Nonempty → (s * t).Nontrivial
source
theorem Set.Nontrivial.add_left {α : Type u_2} [Add α] [IsLeftCancelAdd α] {s t : Set α} :
t.Nontrivial → s.Nonempty → (s + t).Nontrivial
source
theorem Set.Nontrivial.mul {α : Type u_2} [Mul α] [IsLeftCancelMul α] {s t : Set α} (hs : s.Nontrivial) (ht : t.Nontrivial) :
(s * t).Nontrivial
source
theorem Set.Nontrivial.add {α : Type u_2} [Add α] [IsLeftCancelAdd α] {s t : Set α} (hs : s.Nontrivial) (ht : t.Nontrivial) :
(s + t).Nontrivial
source
theorem Set.Nontrivial.mul_right {α : Type u_2} [Mul α] [IsRightCancelMul α] {s t : Set α} :
s.Nontrivial → t.Nonempty → (s * t).Nontrivial
source
theorem Set.Nontrivial.add_right {α : Type u_2} [Add α] [IsRightCancelAdd α] {s t : Set α} :
s.Nontrivial → t.Nonempty → (s + t).Nontrivial
source
theorem Set.Nontrivial.pow {α : Type u_2} [CancelMonoid α] {s : Set α} (hs : s.Nontrivial) {n : ℕ} :
n ≠ 0 → (s ^ n).Nontrivial
source
theorem Set.Nontrivial.nsmul {α : Type u_2} [AddCancelMonoid α] {s : Set α} (hs : s.Nontrivial) {n : ℕ} :
n ≠ 0 → (n • s).Nontrivial
source
def Set.commMonoid {α : Type u_2} [CommMonoid α] :
CommMonoid (Set α)

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

Equations

- Set.commMonoid = { toMonoid := Set.monoid, mul_comm := ⋯ }

Instances For

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

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

Equations

- Set.addCommMonoid = { toAddMonoid := Set.addMonoid, add_comm := ⋯ }

Instances For

source
theorem Set.mul_eq_one_iff {α : Type u_2} [DivisionMonoid α] {s t : Set α} :
s * t = 1 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a * b = 1
source
theorem Set.add_eq_zero_iff {α : Type u_2} [SubtractionMonoid α] {s t : Set α} :
s + t = 0 ↔ ∃ (a : α) (b : α), s = {a} ∧ t = {b} ∧ a + b = 0
source
def Set.divisionMonoid {α : Type u_2} [DivisionMonoid α] :
DivisionMonoid (Set α)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Set.isUnit_iff {α : Type u_2} [DivisionMonoid α] {s : Set α} :
IsUnit s ↔ ∃ (a : α), s = {a} ∧ IsUnit a
source
@[simp]
theorem Set.isAddUnit_iff {α : Type u_2} [SubtractionMonoid α] {s : Set α} :
IsAddUnit s ↔ ∃ (a : α), s = {a} ∧ IsAddUnit a
source
@[simp]
theorem Set.univ_div_univ {α : Type u_2} [DivisionMonoid α] :
univ / univ = univ
source
@[simp]
theorem Set.univ_sub_univ {α : Type u_2} [SubtractionMonoid α] :
univ - univ = univ
source
theorem Set.subset_div_left {α : Type u_2} [DivisionMonoid α] {s t : Set α} (ht : 1 ∈ t) :
s ⊆ s / t
source
theorem Set.subset_sub_left {α : Type u_2} [SubtractionMonoid α] {s t : Set α} (ht : 0 ∈ t) :
s ⊆ s - t
source
theorem Set.inv_subset_div_right {α : Type u_2} [DivisionMonoid α] {s t : Set α} (hs : 1 ∈ s) :
t⁻¹ ⊆ s / t
source
theorem Set.neg_subset_sub_right {α : Type u_2} [SubtractionMonoid α] {s t : Set α} (hs : 0 ∈ s) :
-t ⊆ s - t
source
@[simp]
theorem Set.empty_zpow {α : Type u_2} [DivisionMonoid α] {n : ℤ} (hn : n ≠ 0) :
∅ ^ n = ∅
source
@[simp]
theorem Set.zsmul_empty {α : Type u_2} [SubtractionMonoid α] {n : ℤ} (hn : n ≠ 0) :
n • ∅ = ∅
source
theorem Set.Nonempty.zpow {α : Type u_2} [DivisionMonoid α] {s : Set α} (hs : s.Nonempty) {n : ℤ} :
(s ^ n).Nonempty
source
theorem Set.Nonempty.zsmul {α : Type u_2} [SubtractionMonoid α] {s : Set α} (hs : s.Nonempty) {n : ℤ} :
(n • s).Nonempty
source
@[simp]
theorem Set.zpow_eq_empty {α : Type u_2} [DivisionMonoid α] {s : Set α} {n : ℤ} :
s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0
source
@[simp]
theorem Set.zsmul_eq_empty {α : Type u_2} [SubtractionMonoid α] {s : Set α} {n : ℤ} :
n • s = ∅ ↔ s = ∅ ∧ n ≠ 0
source
@[simp]
theorem Set.singleton_zpow {α : Type u_2} [DivisionMonoid α] (a : α) (n : ℤ) :
{a} ^ n = {a ^ n}
source
@[simp]
theorem Set.zsmul_singleton {α : Type u_2} [SubtractionMonoid α] (a : α) (n : ℤ) :
n • {a} = {n • a}
source
def Set.divisionCommMonoid {α : Type u_2} [DivisionCommMonoid α] :
DivisionCommMonoid (Set α)

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

Equations

- Set.divisionCommMonoid = { toDivisionMonoid := Set.divisionMonoid, mul_comm := ⋯ }

Instances For

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

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

Equations

- Set.subtractionCommMonoid = { toSubtractionMonoid := Set.subtractionMonoid, add_comm := ⋯ }

Instances For

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

source
@[simp]
theorem Set.one_mem_div_iff {α : Type u_2} [Group α] {s t : Set α} :
1 ∈ s / t ↔ ¬Disjoint s t
source
@[simp]
theorem Set.zero_mem_sub_iff {α : Type u_2} [AddGroup α] {s t : Set α} :
0 ∈ s - t ↔ ¬Disjoint s t
source
@[simp]
theorem Set.one_mem_inv_mul_iff {α : Type u_2} [Group α] {s t : Set α} :
1 ∈ t⁻¹ * s ↔ ¬Disjoint s t
source
@[simp]
theorem Set.zero_mem_neg_add_iff {α : Type u_2} [AddGroup α] {s t : Set α} :
0 ∈ -t + s ↔ ¬Disjoint s t
source
theorem Set.one_notMem_div_iff {α : Type u_2} [Group α] {s t : Set α} :
1 ∉ s / t ↔ Disjoint s t
source
theorem Set.zero_notMem_sub_iff {α : Type u_2} [AddGroup α] {s t : Set α} :
0 ∉ s - t ↔ Disjoint s t
source
@[deprecated Set.zero_notMem_sub_iff (since := "2025-05-23")]
theorem Set.not_zero_mem_sub_iff {α : Type u_2} [AddGroup α] {s t : Set α} :
0 ∉ s - t ↔ Disjoint s t

Alias of `Set.zero_notMem_sub_iff`.

source
@[deprecated Set.one_notMem_div_iff (since := "2025-05-23")]
theorem Set.not_one_mem_div_iff {α : Type u_2} [Group α] {s t : Set α} :
1 ∉ s / t ↔ Disjoint s t

Alias of `Set.one_notMem_div_iff`.

source
theorem Set.one_notMem_inv_mul_iff {α : Type u_2} [Group α] {s t : Set α} :
1 ∉ t⁻¹ * s ↔ Disjoint s t
source
theorem Set.zero_notMem_neg_add_iff {α : Type u_2} [AddGroup α] {s t : Set α} :
0 ∉ -t + s ↔ Disjoint s t
source
@[deprecated Set.zero_notMem_neg_add_iff (since := "2025-05-23")]
theorem Set.not_zero_mem_neg_add_iff {α : Type u_2} [AddGroup α] {s t : Set α} :
0 ∉ -t + s ↔ Disjoint s t

Alias of `Set.zero_notMem_neg_add_iff`.

source
@[deprecated Set.one_notMem_inv_mul_iff (since := "2025-05-23")]
theorem Set.not_one_mem_inv_mul_iff {α : Type u_2} [Group α] {s t : Set α} :
1 ∉ t⁻¹ * s ↔ Disjoint s t

Alias of `Set.one_notMem_inv_mul_iff`.

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

Alias of the reverse direction of `Set.one_notMem_div_iff`.

source
theorem Disjoint.zero_notMem_sub_set {α : Type u_2} [AddGroup α] {s t : Set α} :
Disjoint s t → 0 ∉ s - t
source
@[deprecated Disjoint.zero_notMem_sub_set (since := "2025-05-23")]
theorem Disjoint.zero_not_mem_sub_set {α : Type u_2} [AddGroup α] {s t : Set α} :
Disjoint s t → 0 ∉ s - t

Alias of `Disjoint.zero_notMem_sub_set`.

source
@[deprecated Disjoint.one_notMem_div_set (since := "2025-05-23")]
theorem Disjoint.one_not_mem_div_set {α : Type u_2} [Group α] {s t : Set α} :
Disjoint s t → 1 ∉ s / t

Alias of the reverse direction of `Set.one_notMem_div_iff`.

Alias of the reverse direction of `Set.one_notMem_div_iff`.

source
theorem Set.Nonempty.one_mem_div {α : Type u_2} [Group α] {s : Set α} (h : s.Nonempty) :
1 ∈ s / s
source
theorem Set.Nonempty.zero_mem_sub {α : Type u_2} [AddGroup α] {s : Set α} (h : s.Nonempty) :
0 ∈ s - s
source
theorem Set.isUnit_singleton {α : Type u_2} [Group α] (a : α) :
IsUnit {a}
source
theorem Set.isAddUnit_singleton {α : Type u_2} [AddGroup α] (a : α) :
IsAddUnit {a}
source
@[simp]
theorem Set.isUnit_iff_singleton {α : Type u_2} [Group α] {s : Set α} :
IsUnit s ↔ ∃ (a : α), s = {a}
source
@[simp]
theorem Set.isAddUnit_iff_singleton {α : Type u_2} [AddGroup α] {s : Set α} :
IsAddUnit s ↔ ∃ (a : α), s = {a}
source
@[simp]
theorem Set.image_mul_left {α : Type u_2} [Group α] {t : Set α} {a : α} :
(fun (x : α) => a * x) '' t = (fun (x : α) => a⁻¹ * x) ⁻¹' t
source
@[simp]
theorem Set.image_add_left {α : Type u_2} [AddGroup α] {t : Set α} {a : α} :
(fun (x : α) => a + x) '' t = (fun (x : α) => -a + x) ⁻¹' t
source
@[simp]
theorem Set.image_mul_right {α : Type u_2} [Group α] {t : Set α} {b : α} :
(fun (x : α) => x * b) '' t = (fun (x : α) => x * b⁻¹) ⁻¹' t
source
@[simp]
theorem Set.image_add_right {α : Type u_2} [AddGroup α] {t : Set α} {b : α} :
(fun (x : α) => x + b) '' t = (fun (x : α) => x + -b) ⁻¹' t
source
theorem Set.image_mul_left' {α : Type u_2} [Group α] {t : Set α} {a : α} :
(fun (x : α) => a⁻¹ * x) '' t = (fun (x : α) => a * x) ⁻¹' t
source
theorem Set.image_add_left' {α : Type u_2} [AddGroup α] {t : Set α} {a : α} :
(fun (x : α) => -a + x) '' t = (fun (x : α) => a + x) ⁻¹' t
source
theorem Set.image_mul_right' {α : Type u_2} [Group α] {t : Set α} {b : α} :
(fun (x : α) => x * b⁻¹) '' t = (fun (x : α) => x * b) ⁻¹' t
source
theorem Set.image_add_right' {α : Type u_2} [AddGroup α] {t : Set α} {b : α} :
(fun (x : α) => x + -b) '' t = (fun (x : α) => x + b) ⁻¹' t
source
@[simp]
theorem Set.preimage_mul_left_singleton {α : Type u_2} [Group α] {a b : α} :
(fun (x : α) => a * x) ⁻¹' {b} = {a⁻¹ * b}
source
@[simp]
theorem Set.preimage_add_left_singleton {α : Type u_2} [AddGroup α] {a b : α} :
(fun (x : α) => a + x) ⁻¹' {b} = {-a + b}
source
@[simp]
theorem Set.preimage_mul_right_singleton {α : Type u_2} [Group α] {a b : α} :
(fun (x : α) => x * a) ⁻¹' {b} = {b * a⁻¹}
source
@[simp]
theorem Set.preimage_add_right_singleton {α : Type u_2} [AddGroup α] {a b : α} :
(fun (x : α) => x + a) ⁻¹' {b} = {b + -a}
source
@[simp]
theorem Set.preimage_mul_left_one {α : Type u_2} [Group α] {a : α} :
(fun (x : α) => a * x) ⁻¹' 1 = {a⁻¹}
source
@[simp]
theorem Set.preimage_add_left_zero {α : Type u_2} [AddGroup α] {a : α} :
(fun (x : α) => a + x) ⁻¹' 0 = {-a}
source
@[simp]
theorem Set.preimage_mul_right_one {α : Type u_2} [Group α] {b : α} :
(fun (x : α) => x * b) ⁻¹' 1 = {b⁻¹}
source
@[simp]
theorem Set.preimage_add_right_zero {α : Type u_2} [AddGroup α] {b : α} :
(fun (x : α) => x + b) ⁻¹' 0 = {-b}
source
theorem Set.preimage_mul_left_one' {α : Type u_2} [Group α] {a : α} :
(fun (x : α) => a⁻¹ * x) ⁻¹' 1 = {a}
source
theorem Set.preimage_add_left_zero' {α : Type u_2} [AddGroup α] {a : α} :
(fun (x : α) => -a + x) ⁻¹' 0 = {a}
source
theorem Set.preimage_mul_right_one' {α : Type u_2} [Group α] {b : α} :
(fun (x : α) => x * b⁻¹) ⁻¹' 1 = {b}
source
theorem Set.preimage_add_right_zero' {α : Type u_2} [AddGroup α] {b : α} :
(fun (x : α) => x + -b) ⁻¹' 0 = {b}
source
@[simp]
theorem Set.mul_univ {α : Type u_2} [Group α] {s : Set α} (hs : s.Nonempty) :
s * univ = univ
source
@[simp]
theorem Set.add_univ {α : Type u_2} [AddGroup α] {s : Set α} (hs : s.Nonempty) :
s + univ = univ
source
@[simp]
theorem Set.univ_mul {α : Type u_2} [Group α] {t : Set α} (ht : t.Nonempty) :
univ * t = univ
source
@[simp]
theorem Set.univ_add {α : Type u_2} [AddGroup α] {t : Set α} (ht : t.Nonempty) :
univ + t = univ
source
theorem Set.image_inv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Set α) :
⇑f '' s⁻¹ = (⇑f '' s)⁻¹
source
theorem Set.image_neg {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Set α) :
⇑f '' (-s) = -⇑f '' s
source
theorem Set.image_mul {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) {s t : Set α} :
⇑m '' (s * t) = ⇑m '' s * ⇑m '' t
source
theorem Set.image_add {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) {s t : Set α} :
⇑m '' (s + t) = ⇑m '' s + ⇑m '' t
source
theorem Set.mul_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [FunLike F α β] [MulHomClass F α β] (m : F) {s t : Set β} (hs : s ⊆ range ⇑m) (ht : t ⊆ range ⇑m) :
s * t ⊆ range ⇑m
source
theorem Set.add_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [FunLike F α β] [AddHomClass F α β] (m : F) {s t : Set β} (hs : s ⊆ range ⇑m) (ht : t ⊆ range ⇑m) :
s + t ⊆ range ⇑m
source
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 t : Set β} :
⇑m ⁻¹' s * ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s * t)
source
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 t : Set β} :
⇑m ⁻¹' s + ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s + t)
source
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 t : Set β} (hs : s ⊆ range ⇑m) (ht : t ⊆ range ⇑m) :
⇑m ⁻¹' (s * t) = ⇑m ⁻¹' s * ⇑m ⁻¹' t
source
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 t : Set β} (hs : s ⊆ range ⇑m) (ht : t ⊆ range ⇑m) :
⇑m ⁻¹' (s + t) = ⇑m ⁻¹' s + ⇑m ⁻¹' t
source
theorem Set.image_pow_of_ne_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] [FunLike F α β] [MulHomClass F α β] {n : ℕ} :
n ≠ 0 → ∀ (f : F) (s : Set α), ⇑f '' (s ^ n) = (⇑f '' s) ^ n
source
theorem Set.image_nsmul_of_ne_zero {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddHomClass F α β] {n : ℕ} :
n ≠ 0 → ∀ (f : F) (s : Set α), ⇑f '' (n • s) = n • ⇑f '' s
source
theorem Set.image_pow {F : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Set α) (n : ℕ) :
⇑f '' (s ^ n) = (⇑f '' s) ^ n
source
theorem Set.image_nsmul {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Set α) (n : ℕ) :
⇑f '' (n • s) = n • ⇑f '' s
source
theorem Set.image_div {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {s t : Set α} :
⇑m '' (s / t) = ⇑m '' s / ⇑m '' t
source
theorem Set.image_sub {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s t : Set α} :
⇑m '' (s - t) = ⇑m '' s - ⇑m '' t
source
theorem Set.div_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] [FunLike F α β] [MonoidHomClass F α β] (m : F) {s t : Set β} (hs : s ⊆ range ⇑m) (ht : t ⊆ range ⇑m) :
s / t ⊆ range ⇑m
source
theorem Set.sub_subset_range {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] [FunLike F α β] [AddMonoidHomClass F α β] (m : F) {s t : Set β} (hs : s ⊆ range ⇑m) (ht : t ⊆ range ⇑m) :
s - t ⊆ range ⇑m
source
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 t : Set β} :
⇑m ⁻¹' s / ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s / t)
source
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 t : Set β} :
⇑m ⁻¹' s - ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s - t)
source
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 t : Set β} (hs : s ⊆ range ⇑m) (ht : t ⊆ range ⇑m) :
⇑m ⁻¹' (s / t) = ⇑m ⁻¹' s / ⇑m ⁻¹' t
source
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 t : Set β} (hs : s ⊆ range ⇑m) (ht : t ⊆ range ⇑m) :
⇑m ⁻¹' (s - t) = ⇑m ⁻¹' s - ⇑m ⁻¹' t
source
@[simp]
theorem Set.inv_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Inv (α i)] (s : Set ι) (t : (i : ι) → Set (α i)) :
(s.pi t)⁻¹ = s.pi fun (i : ι) => (t i)⁻¹
source
@[simp]
theorem Set.neg_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → Neg (α i)] (s : Set ι) (t : (i : ι) → Set (α i)) :
-s.pi t = s.pi fun (i : ι) => -t i
source
theorem Set.MapsTo.mul {α : Type u_2} {β : Type u_3} [Mul β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) :
MapsTo (f₁ * f₂) A (B₁ * B₂)
source
theorem Set.MapsTo.add {α : Type u_2} {β : Type u_3} [Add β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) :
MapsTo (f₁ + f₂) A (B₁ + B₂)
source
theorem Set.MapsTo.inv {α : Type u_2} {β : Type u_3} [InvolutiveInv β] {A : Set α} {B : Set β} {f : α → β} (h : MapsTo f A B) :
MapsTo f⁻¹ A B⁻¹
source
theorem Set.MapsTo.neg {α : Type u_2} {β : Type u_3} [InvolutiveNeg β] {A : Set α} {B : Set β} {f : α → β} (h : MapsTo f A B) :
MapsTo (-f) A (-B)
source
theorem Set.MapsTo.div {α : Type u_2} {β : Type u_3} [Div β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) :
MapsTo (f₁ / f₂) A (B₁ / B₂)
source
theorem Set.MapsTo.sub {α : Type u_2} {β : Type u_3} [Sub β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : MapsTo f₁ A B₁) (h₂ : MapsTo f₂ A B₂) :
MapsTo (f₁ - f₂) A (B₁ - B₂)